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

Theorem imim12i 55
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 30 1  |-  ( ( ps  ->  ch )  ->  ( ph  ->  th )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4
This theorem is referenced by:  imim1i  56  dedlem0b  920  meredith  1410  19.38OLD  1891  exmoeu  2296  pssnn  7286  kmlem1  7986  brdom5  8363  brdom4  8364  axpowndlem2  8429  naim1  26038  naim2  26039  meran1  26065  ax10ext  27474
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator