HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version
Theorem imim12i 18
Description: Inference joining two implications.
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.2 . . 3 |- (ch -> th)
21imim2i 17 . 2 |- ((ps -> ch) -> (ps -> th))
3 imim12i.1 . . 3 |- (ph -> ps)
43imim1i 16 . 2 |- ((ps -> th) -> (ph -> th))
52, 4syl 10 1 |- ((ps -> ch) -> (ph -> th))
Colors of variables: wff set class
Syntax hints:   -> wi 3
This theorem is referenced by:  pm5.75 747  dedlem0b 759  19.38 1077  exmoeu 1406  iununi 2606  pssnn 4513  kmlem1 4737  zorn 4769  brdom5 4774  brdom4 4775  axpowndlem2 4922  dfuz 6150  cau5i 6854
This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-mp 7
Copyright terms: Public domain