Theorem jca31 309

Description: Join three consequents. (Contributed by Jeff Hankins, 1-Aug-2009.)

Hypotheses

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

Assertion

Ref	Expression
jca31	⊢ (𝜑 → ((𝜓 ∧ 𝜒) ∧ 𝜃))

Proof of Theorem jca31

Step	Hyp	Ref	Expression
1		jca31.1	. . 3 ⊢ (𝜑 → 𝜓)
2		jca31.2	. . 3 ⊢ (𝜑 → 𝜒)
3	1, 2	jca 306	. 2 ⊢ (𝜑 → (𝜓 ∧ 𝜒))
4		jca31.3	. 2 ⊢ (𝜑 → 𝜃)
5	3, 4	jca 306	1 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) ∧ 𝜃))

Syntax hints:   → wi 4   ∧ wa 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 108

This theorem is referenced by:  3jca  1204  syl21anbrc  1209  syl21anc  1273  f1oiso2  5978  exmidapne  7522  nnnq0lem1  7709  prmuloc  7829  suplocexprlemex  7985  prsrlem1  8005  apreap  8809  lemulge11  9088  elnnz  9533  supinfneg  9873  infsupneg  9874  leexp1a  10902  faclbnd6  11052  zfz1isolem1  11150  oddpwdclemdc  12808  ennnfonelemf1  13102  grpidinv2  13704  rhmopp  14254  dvdsrzring  14682  cncnp2m  15025  upgrex  16027  uhgr2edg  16130  bj-charfun  16506