Theorem jcad 301

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 137	. 2 ⊢ (𝜒 → (𝜃 → (𝜒 ∧ 𝜃)))
4	1, 2, 3	syl6c 65	1 ⊢ (𝜑 → (𝜓 → (𝜒 ∧ 𝜃)))

Syntax hints:   → wi 4   ∧ wa 102

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia3 106

This theorem is referenced by:  jctild  309  jctird  310  ancld  318  ancrd  319  anim12ii  335  equsex  1656  equsexd  1657  rexim  2455  rr19.28v  2734  sotricim  4078  sotritrieq  4080  ordsucss  4248  ordpwsucss  4310  peano5  4339  iss  4674  funssres  4962  ssimaex  5255  elpreima  5307  tposfo2  5905  nnmord  6113  enq0tr  6624  addnqprl  6719  addnqpru  6720  cauappcvgprlemdisj  6841  lttri3  7191  ltleap  7730  mulgt1  7941  nominpos  8268  uzind  8458  indstr  8681  eqreznegel  8699  shftuz  9705  caucvgrelemcau  9866  sqrtsq  9930  mulcn2  10151  dvdsgcdb  10402  algcvgblem  10431  lcmdvdsb  10466  rpexp  10532  bj-om  10732