MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  imim12i Structured version   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  1413  19.38OLD  1895  exmoeu  2322  pssnn  7319  kmlem1  8020  brdom5  8397  brdom4  8398  axpowndlem2  8463  naim1  26099  naim2  26100  meran1  26126  ax10ext  27538
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator