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  8330  uzm1  12908  ixxssixx  13398  iccid  13429  iccsplit  13524  fzen  13581  lmodprop2d  21075  fbun  24028  hausflim  24169  icoopnst  25129  iocopnst  25130  abelth  26635  usgr2pth  30153  shsvs  31722  cnlnssadj  32479  fnrelpredd  35516  trssfir1om  35541  trssfir1omregs  35582  cvmlift2lem10  35817  endofsegid  36590  elicc3  36861  areacirclem1  38392  islvol2aN  40399  alrim3con13v  45275  ormkglobd  47624  bgoldbtbndlem4  48606