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  1179  syl21anbrc  1184  syl21anc  1248  f1oiso2  5875  exmidapne  7330  nnnq0lem1  7516  prmuloc  7636  suplocexprlemex  7792  prsrlem1  7812  apreap  8617  lemulge11  8896  elnnz  9339  supinfneg  9672  infsupneg  9673  leexp1a  10689  faclbnd6  10839  zfz1isolem1  10935  oddpwdclemdc  12352  ennnfonelemf1  12646  grpidinv2  13216  rhmopp  13758  dvdsrzring  14185  cncnp2m  14493  bj-charfun  15479