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  1774  equsexd  1775  rexim  2624  rr19.28v  2944  sotricim  4418  sotritrieq  4420  ordsucss  4600  ordpwsucss  4663  peano5  4694  iss  5057  funssres  5366  ssimaex  5703  elpreima  5762  resflem  5807  tposfo2  6428  nnmord  6680  map0g  6852  mapsn  6854  enq0tr  7647  addnqprl  7742  addnqpru  7743  cauappcvgprlemdisj  7864  lttri3  8252  ltleap  8805  mulgt1  9036  nominpos  9375  uzind  9584  indstr  9820  eqreznegel  9841  ccatopth  11290  shftuz  11371  caucvgrelemcau  11534  sqrtsq  11598  mulcn2  11866  dvdsgcdb  12577  algcvgblem  12614  lcmdvdsb  12649  rpexp  12718  infpnlem1  12925  imasring  14070  unitmulclb  14121  cnntr  14942  cnrest2  14953  txlm  14996  metrest  15223  uspgr2wlkeq  16176  bj-om  16482