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

Theorem imim12i 56
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 14 . 2  |-  ( ( ps  ->  ch )  ->  ( ps  ->  th )
)
41, 3syl5 31 1  |-  ( ( ps  ->  ch )  ->  ( ph  ->  th )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4
This theorem is referenced by:  imim1i  57  dedlem0b  921  meredith  1414  19.38OLD  1896  exmoeu  2325  pssnn  7329  kmlem1  8032  brdom5  8409  brdom4  8410  axpowndlem2  8475  naim1  26136  naim2  26137  meran1  26163  ax10ext  27585
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator