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  6543  nnmord  6795  map0g  6974  mapsn  6978  enq0tr  7808  addnqprl  7903  addnqpru  7904  cauappcvgprlemdisj  8025  lttri3  8412  ltleap  8969  mulgt1  9202  nominpos  9555  uzind  9768  indstr  10009  eqreznegel  10030  ccatopth  11510  shftuz  11604  caucvgrelemcau  11768  sqrtsq  11832  mulcn2  12103  dvdsgcdb  12815  algcvgblem  12852  lcmdvdsb  12887  rpexp  12957  infpnlem1  13167  imasring  14478  unitmulclb  14530  assapropd  15123  cnntr  15484  cnrest2  15495  txlm  15538  metrest  15765  bposlem7  16350  uspgr2wlkeq  16844  bj-om  17201