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  4414  sotritrieq  4416  ordsucss  4596  ordpwsucss  4659  peano5  4690  iss  5051  funssres  5360  ssimaex  5697  elpreima  5756  resflem  5801  tposfo2  6419  nnmord  6671  map0g  6843  mapsn  6845  enq0tr  7629  addnqprl  7724  addnqpru  7725  cauappcvgprlemdisj  7846  lttri3  8234  ltleap  8787  mulgt1  9018  nominpos  9357  uzind  9566  indstr  9796  eqreznegel  9817  ccatopth  11256  shftuz  11336  caucvgrelemcau  11499  sqrtsq  11563  mulcn2  11831  dvdsgcdb  12542  algcvgblem  12579  lcmdvdsb  12614  rpexp  12683  infpnlem1  12890  imasring  14035  unitmulclb  14086  cnntr  14907  cnrest2  14918  txlm  14961  metrest  15188  uspgr2wlkeq  16086  bj-om  16324