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  2636  rr19.28v  2956  sotricim  4443  sotritrieq  4445  ordsucss  4625  ordpwsucss  4688  peano5  4719  iss  5083  funssres  5394  ssimaex  5737  elpreima  5796  resflem  5840  tposfo2  6497  nnmord  6749  map0g  6921  mapsn  6924  enq0tr  7748  addnqprl  7843  addnqpru  7844  cauappcvgprlemdisj  7965  lttri3  8352  ltleap  8905  mulgt1  9136  nominpos  9475  uzind  9688  indstr  9924  eqreznegel  9945  ccatopth  11404  shftuz  11498  caucvgrelemcau  11661  sqrtsq  11725  mulcn2  11993  dvdsgcdb  12705  algcvgblem  12742  lcmdvdsb  12777  rpexp  12846  infpnlem1  13053  imasring  14200  unitmulclb  14251  cnntr  15082  cnrest2  15093  txlm  15136  metrest  15363  uspgr2wlkeq  16352  bj-om  16699