Theorem 3jcad 1147

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 412	. . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
3		3jcad.2	. . . 4 ⊢ (𝜑 → (𝜓 → 𝜃))
4	3	imp 412	. . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝜃)
5		3jcad.3	. . . 4 ⊢ (𝜑 → (𝜓 → 𝜏))
6	5	imp 412	. . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝜏)
7	2, 4, 6	3jca 1146	. 2 ⊢ ((𝜑 ∧ 𝜓) → (𝜒 ∧ 𝜃 ∧ 𝜏))
8	7	ex 418	1 ⊢ (𝜑 → (𝜓 → (𝜒 ∧ 𝜃 ∧ 𝜏)))

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  onfununi  8385  uzm1  13037  ixxssixx  13528  iccid  13559  iccsplit  13654  fzen  13712  lmodprop2d  21241  fbun  24203  hausflim  24344  icoopnst  25304  iocopnst  25305  abelth  26814  usgr2pth  30396  shsvs  31971  cnlnssadj  32728  fnrelpredd  35838  trssfihf  35853  trssfihfregs  35938  cvmlift2lem10  36278  endofsegid  37058  elicc3  37313  areacirclem1  38887  islvol2aN  40908  alrim3con13v  45770  ormkglobd  48154  bgoldbtbndlem4  49173