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  1203  syl21anbrc  1208  syl21anc  1272  f1oiso2  5967  exmidapne  7478  nnnq0lem1  7665  prmuloc  7785  suplocexprlemex  7941  prsrlem1  7961  apreap  8766  lemulge11  9045  elnnz  9488  supinfneg  9828  infsupneg  9829  leexp1a  10855  faclbnd6  11005  zfz1isolem1  11103  oddpwdclemdc  12744  ennnfonelemf1  13038  grpidinv2  13640  rhmopp  14189  dvdsrzring  14616  cncnp2m  14954  upgrex  15953  uhgr2edg  16056  bj-charfun  16402