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  1780  equsexd  1782  rexim  2644  rr19.28v  2966  sotricim  4466  sotritrieq  4468  ordsucss  4649  ordpwsucss  4712  peano5  4743  iss  5107  funssres  5418  ssimaex  5761  elpreima  5822  resflem  5866  tposfo2  6532  nnmord  6784  map0g  6963  mapsn  6966  enq0tr  7795  addnqprl  7890  addnqpru  7891  cauappcvgprlemdisj  8012  lttri3  8399  ltleap  8954  mulgt1  9187  nominpos  9526  uzind  9740  indstr  9976  eqreznegel  9997  ccatopth  11471  shftuz  11565  caucvgrelemcau  11729  sqrtsq  11793  mulcn2  12061  dvdsgcdb  12773  algcvgblem  12810  lcmdvdsb  12845  rpexp  12914  infpnlem1  13121  imasring  14352  unitmulclb  14404  assapropd  14997  cnntr  15309  cnrest2  15320  txlm  15363  metrest  15590  uspgr2wlkeq  16589  bj-om  16946