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  6000  exmidapne  7574  nnnq0lem1  7761  prmuloc  7881  suplocexprlemex  8037  prsrlem1  8057  apreap  8861  lemulge11  9140  elnnz  9587  supinfneg  9927  infsupneg  9928  leexp1a  10956  faclbnd6  11106  zfz1isolem1  11212  oddpwdclemdc  12870  ennnfonelemf1  13169  grpidinv2  13771  rhmopp  14321  dvdsrzring  14751  cncnp2m  15096  upgrex  16098  uhgr2edg  16201  bj-charfun  16577