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  1180  syl21anbrc  1185  syl21anc  1249  f1oiso2  5909  exmidapne  7392  nnnq0lem1  7579  prmuloc  7699  suplocexprlemex  7855  prsrlem1  7875  apreap  8680  lemulge11  8959  elnnz  9402  supinfneg  9736  infsupneg  9737  leexp1a  10761  faclbnd6  10911  zfz1isolem1  11007  oddpwdclemdc  12570  ennnfonelemf1  12864  grpidinv2  13465  rhmopp  14013  dvdsrzring  14440  cncnp2m  14778  upgrex  15774  bj-charfun  15881