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  8342  uzm1  12992  ixxssixx  13483  iccid  13514  iccsplit  13609  fzen  13667  lmodprop2d  21192  fbun  24152  hausflim  24293  icoopnst  25253  iocopnst  25254  abelth  26761  usgr2pth  30343  shsvs  31918  cnlnssadj  32675  fnrelpredd  35709  trssfir1om  35726  trssfir1omregs  35787  cvmlift2lem10  36056  endofsegid  36830  elicc3  37085  areacirclem1  38606  islvol2aN  40629  alrim3con13v  45501  ormkglobd  47856  bgoldbtbndlem4  48875