Theorem jcad 307

Description: Deduction conjoining the consequents of two implications. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 23-Jul-2013.)

Hypotheses

Ref	Expression
jcad.1	⊢ (𝜑 → (𝜓 → 𝜒))
jcad.2	⊢ (𝜑 → (𝜓 → 𝜃))

Assertion

Ref	Expression
jcad	⊢ (𝜑 → (𝜓 → (𝜒 ∧ 𝜃)))

Proof of Theorem jcad

Step	Hyp	Ref	Expression
1		jcad.1	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
2		jcad.2	. 2 ⊢ (𝜑 → (𝜓 → 𝜃))
3		pm3.2 139	. 2 ⊢ (𝜒 → (𝜃 → (𝜒 ∧ 𝜃)))
4	1, 2, 3	syl6c 66	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:  jca2  308  jctild  316  jctird  317  ancld  325  ancrd  326  anim12ii  343  equsex  1780  equsexd  1782  rexim  2644  rr19.28v  2966  sotricim  4470  sotritrieq  4472  ordsucss  4653  ordpwsucss  4716  peano5  4747  iss  5112  funssres  5423  ssimaex  5767  elpreima  5831  resflem  5875  tposfo2  6542  nnmord  6794  map0g  6973  mapsn  6977  enq0tr  7808  addnqprl  7903  addnqpru  7904  cauappcvgprlemdisj  8025  lttri3  8412  ltleap  8969  mulgt1  9202  nominpos  9555  uzind  9769  indstr  10010  eqreznegel  10031  ccatopth  11511  shftuz  11605  caucvgrelemcau  11769  sqrtsq  11833  mulcn2  12104  dvdsgcdb  12816  algcvgblem  12853  lcmdvdsb  12888  rpexp  12958  infpnlem1  13168  imasring  14479  unitmulclb  14531  assapropd  15124  cnntr  15463  cnrest2  15474  txlm  15517  metrest  15744  bposlem7  16329  uspgr2wlkeq  16823  bj-om  17180