Theorem 3jcad 1243

Description: Deduction conjoining the consequents of three implications. (Contributed by NM, 25-Sep-2005.)

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 445	. . 3 |- ( ( ph /\ ps ) -> ch )
3		3jcad.2	. . . 4 |- ( ph -> ( ps -> th ) )
4	3	imp 445	. . 3 |- ( ( ph /\ ps ) -> th )
5		3jcad.3	. . . 4 |- ( ph -> ( ps -> ta ) )
6	5	imp 445	. . 3 |- ( ( ph /\ ps ) -> ta )
7	2, 4, 6	3jca 1242	. 2 |- ( ( ph /\ ps ) -> ( ch /\ th /\ ta ) )
8	7	ex 450	1 |- ( ph -> ( ps -> ( ch /\ th /\ ta ) ) )

Syntax hints:   -> wi 4   /\ wa 384   /\ w3a 1037

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

This theorem depends on definitions:  df-bi 197  df-an 386  df-3an 1039

This theorem is referenced by:  onfununi  7438  uzm1  11718  ixxssixx  12189  iccid  12220  iccsplit  12305  fzen  12358  lmodprop2d  18925  fbun  21644  hausflim  21785  icoopnst  22738  iocopnst  22739  abelth  24195  usgr2pth  26660  shsvs  28182  cnlnssadj  28939  cvmlift2lem10  31294  endofsegid  32192  elicc3  32311  areacirclem1  33500  islvol2aN  34878  alrim3con13v  38743  bgoldbtbndlem4  41696