Theorem 3jcad 1129

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

Hypotheses

Ref	Expression
3jcad.1	⊢ (𝜑 → (𝜓 → 𝜒))
3jcad.2	⊢ (𝜑 → (𝜓 → 𝜃))
3jcad.3	⊢ (𝜑 → (𝜓 → 𝜏))

Assertion

Ref	Expression
3jcad	⊢ (𝜑 → (𝜓 → (𝜒 ∧ 𝜃 ∧ 𝜏)))

Proof of Theorem 3jcad

Step	Hyp	Ref	Expression
1		3jcad.1	. . . 4 ⊢ (𝜑 → (𝜓 → 𝜒))
2	1	imp 406	. . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
3		3jcad.2	. . . 4 ⊢ (𝜑 → (𝜓 → 𝜃))
4	3	imp 406	. . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝜃)
5		3jcad.3	. . . 4 ⊢ (𝜑 → (𝜓 → 𝜏))
6	5	imp 406	. . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝜏)
7	2, 4, 6	3jca 1128	. 2 ⊢ ((𝜑 ∧ 𝜓) → (𝜒 ∧ 𝜃 ∧ 𝜏))
8	7	ex 412	1 ⊢ (𝜑 → (𝜓 → (𝜒 ∧ 𝜃 ∧ 𝜏)))

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086

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 207  df-an 396  df-3an 1088

This theorem is referenced by:  onfununi  8273  uzm1  12785  ixxssixx  13275  iccid  13306  iccsplit  13401  fzen  13457  lmodprop2d  20875  fbun  23784  hausflim  23925  icoopnst  24892  iocopnst  24893  abelth  26407  usgr2pth  29837  shsvs  31398  cnlnssadj  32155  fnrelpredd  35247  trssfir1om  35267  trssfir1omregs  35292  cvmlift2lem10  35506  endofsegid  36279  elicc3  36511  areacirclem1  37909  islvol2aN  39852  alrim3con13v  44774  ormkglobd  47119  bgoldbtbndlem4  48054