Theorem 3jcad 1141

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

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1097

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 209  df-an 400  df-3an 1099

This theorem is referenced by:  onfununi  8306  uzm1  12867  ixxssixx  13357  iccid  13388  iccsplit  13483  fzen  13540  lmodprop2d  20979  fbun  23888  hausflim  24029  icoopnst  24989  iocopnst  24990  abelth  26492  usgr2pth  29921  shsvs  31483  cnlnssadj  32240  fnrelpredd  35348  trssfir1om  35368  trssfir1omregs  35393  cvmlift2lem10  35623  endofsegid  36396  elicc3  36638  areacirclem1  38168  islvol2aN  40177  alrim3con13v  45070  ormkglobd  47412  bgoldbtbndlem4  48391