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  5870  exmidapne  7320  nnnq0lem1  7506  prmuloc  7626  suplocexprlemex  7782  prsrlem1  7802  apreap  8606  lemulge11  8885  elnnz  9327  supinfneg  9660  infsupneg  9661  leexp1a  10665  faclbnd6  10815  zfz1isolem1  10911  oddpwdclemdc  12311  ennnfonelemf1  12575  grpidinv2  13130  rhmopp  13672  dvdsrzring  14091  cncnp2m  14399  bj-charfun  15299