Theorem 3jcad 1051

Description: Deduction conjoining the consequents of three implications.

Hypotheses

Ref	Expression
3jcad.1	|- (ph -> (ps -> ch))
3jcad.2	|- (ph -> (ps -> th))
3jcad.3	|- (ph -> (ps -> ta))

Assertion

Ref	Expression
3jcad	|- (ph -> (ps -> (ch /\ th /\ ta)))

Proof of Theorem 3jcad

Step	Hyp	Ref	Expression
1		3jcad.1	. . . 4 |- (ph -> (ps -> ch))
2	1	imp 377	. . 3 |- ((ph /\ ps) -> ch)
3		3jcad.2	. . . 4 |- (ph -> (ps -> th))
4	3	imp 377	. . 3 |- ((ph /\ ps) -> th)
5		3jcad.3	. . . 4 |- (ph -> (ps -> ta))
6	5	imp 377	. . 3 |- ((ph /\ ps) -> ta)
7	2, 4, 6	3jca 1050	. 2 |- ((ph /\ ps) -> (ch /\ th /\ ta))
8	7	ex 402	1 |- (ph -> (ps -> (ch /\ th /\ ta)))

Syntax hints:   -> wi 3   /\ wa 240   /\ w3a 858

This theorem is referenced by:  onfununi 5116  19.21a3con13v 5828  fzen 7664  climmulc2 8389  clim2serz 8394  iscau3 9216  iscau4 9218  caussi 9232  lmcau 9274  cnlnssadj 11650  suprzcl 13658  elicc3 15362  ccid 15363  reconnlem5 15450  iccconn 15453  neibastop1 15518  filssufillem 15570  ufinffr 15578  uzm1 15784  fzm1 15796  iccsplit 15854  iccss 15855  icoopnst 15876  iocopnst 15877  ismtyhmeo 15951

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

This theorem depends on definitions:  df-bi 164  df-an 242  df-3an 860

Copyright terms: Public domain