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 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) ∧ 𝜃))

This proof depends on syntax axioms:   → wi 4   ∧ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 108

This theorem is used by:  3jca  1208  syl21anbrc  1213  syl21anc  1277  f1oiso2  6033  exmidapne  7626  nnnq0lem1  7813  prmuloc  7933  suplocexprlemex  8089  prsrlem1  8109  apreap  8915  lemulge11  9196  elnnz  9654  supinfneg  9995  infsupneg  9996  leexp1a  11031  faclbnd6  11182  zfz1isolem1  11292  oddpwdclemdc  12951  ennnfonelemf1  13309  grpidinv2  13863  rhmopp  14483  dvdsrzring  14938  cncnp2m  15332  upgrex  16344  uhgr2edg  16447  bj-charfun  16833