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  6006  exmidapne  7590  nnnq0lem1  7777  prmuloc  7897  suplocexprlemex  8053  prsrlem1  8073  apreap  8878  lemulge11  9157  elnnz  9604  supinfneg  9945  infsupneg  9946  leexp1a  10980  faclbnd6  11131  zfz1isolem1  11237  oddpwdclemdc  12895  ennnfonelemf1  13253  grpidinv2  13813  rhmopp  14421  dvdsrzring  14877  cncnp2m  15222  upgrex  16224  uhgr2edg  16327  bj-charfun  16703