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  2943  sotricim  4415  sotritrieq  4417  ordsucss  4597  ordpwsucss  4660  peano5  4691  iss  5054  funssres  5363  ssimaex  5700  elpreima  5759  resflem  5804  tposfo2  6424  nnmord  6676  map0g  6848  mapsn  6850  enq0tr  7637  addnqprl  7732  addnqpru  7733  cauappcvgprlemdisj  7854  lttri3  8242  ltleap  8795  mulgt1  9026  nominpos  9365  uzind  9574  indstr  9805  eqreznegel  9826  ccatopth  11269  shftuz  11349  caucvgrelemcau  11512  sqrtsq  11576  mulcn2  11844  dvdsgcdb  12555  algcvgblem  12592  lcmdvdsb  12627  rpexp  12696  infpnlem1  12903  imasring  14048  unitmulclb  14099  cnntr  14920  cnrest2  14931  txlm  14974  metrest  15201  uspgr2wlkeq  16137  bj-om  16409