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

Theorem imim12i 57
Description: Inference joining two implications. (Contributed by NM, 12-Mar-1993.) (Proof shortened by Mel L. 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 32 1  |-  ( ( ps  ->  ch )  ->  ( ph  ->  th )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7
This theorem is referenced by:  imim1i  58  dedlem0b  944  meredith  1447  exmoeuOLD  2299  pssnn  7645  kmlem1  8433  brdom5  8810  brdom4  8811  axpowndlem2  8876  axpowndlem2OLD  8877  xrge0infss  26224  naim1  28395  naim2  28396  meran1  28421  axc11next  29828
  Copyright terms: Public domain W3C validator