MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  imim12i Unicode version

Theorem imim12i 53
Description: Inference joining two implications. (Contributed by NM, 5-Aug-1993.) (Proof shortened by O'Cat, 29-Oct-2011.)
Hypotheses
Ref Expression
imim12i.1  |-  ( ph  ->  ps )
imim12i.2  |-  ( ch 
->  th )
Assertion
Ref Expression
imim12i  |-  ( ( ps  ->  ch )  ->  ( ph  ->  th )
)

Proof of Theorem imim12i
StepHypRef Expression
1 imim12i.1 . 2  |-  ( ph  ->  ps )
2 imim12i.2 . . 3  |-  ( ch 
->  th )
32imim2i 13 . 2  |-  ( ( ps  ->  ch )  ->  ( ps  ->  th )
)
41, 3syl5 28 1  |-  ( ( ps  ->  ch )  ->  ( ph  ->  th )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4
This theorem is referenced by:  imim1i  54  dedlem0b  919  meredith  1394  19.38  1810  exmoeu  2185  pssnn  7081  kmlem1  7776  brdom5  8154  brdom4  8155  axpowndlem2  8220  naim1  24823  naim2  24824  meran1  24850  isib2g1a1  26116  isibg1a2  26117  isibg1a3a  26122  isibg1spa  26123  isibg1a5a  26124  ax10ext  27606
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator