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  1777  rexim  2626  rr19.28v  2946  sotricim  4420  sotritrieq  4422  ordsucss  4602  ordpwsucss  4665  peano5  4696  iss  5059  funssres  5369  ssimaex  5707  elpreima  5766  resflem  5811  tposfo2  6433  nnmord  6685  map0g  6857  mapsn  6859  enq0tr  7654  addnqprl  7749  addnqpru  7750  cauappcvgprlemdisj  7871  lttri3  8259  ltleap  8812  mulgt1  9043  nominpos  9382  uzind  9591  indstr  9827  eqreznegel  9848  ccatopth  11301  shftuz  11382  caucvgrelemcau  11545  sqrtsq  11609  mulcn2  11877  dvdsgcdb  12589  algcvgblem  12626  lcmdvdsb  12661  rpexp  12730  infpnlem1  12937  imasring  14083  unitmulclb  14134  cnntr  14955  cnrest2  14966  txlm  15009  metrest  15236  uspgr2wlkeq  16222  bj-om  16558