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

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:  jca2  308  jctild  316  jctird  317  ancld  325  ancrd  326  anim12ii  343  equsex  1776  equsexd  1778  rexim  2638  rr19.28v  2960  sotricim  4449  sotritrieq  4451  ordsucss  4631  ordpwsucss  4694  peano5  4725  iss  5089  funssres  5400  ssimaex  5743  elpreima  5802  resflem  5846  tposfo2  6511  nnmord  6763  map0g  6935  mapsn  6938  enq0tr  7765  addnqprl  7860  addnqpru  7861  cauappcvgprlemdisj  7982  lttri3  8369  ltleap  8924  mulgt1  9157  nominpos  9496  uzind  9710  indstr  9946  eqreznegel  9967  ccatopth  11436  shftuz  11530  caucvgrelemcau  11693  sqrtsq  11757  mulcn2  12025  dvdsgcdb  12737  algcvgblem  12774  lcmdvdsb  12809  rpexp  12878  infpnlem1  13085  imasring  14310  unitmulclb  14362  cnntr  15219  cnrest2  15230  txlm  15273  metrest  15500  uspgr2wlkeq  16489  bj-om  16846