Theorem jcad 305

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

Syntax hints:   → wi 4   ∧ wa 103

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

This theorem is referenced by:  jca2  306  jctild  314  jctird  315  ancld  323  ancrd  324  anim12ii  341  equsex  1707  equsexd  1708  rexim  2529  rr19.28v  2828  sotricim  4253  sotritrieq  4255  ordsucss  4428  ordpwsucss  4490  peano5  4520  iss  4873  funssres  5173  ssimaex  5490  elpreima  5547  resflem  5592  tposfo2  6172  nnmord  6421  map0g  6590  mapsn  6592  enq0tr  7266  addnqprl  7361  addnqpru  7362  cauappcvgprlemdisj  7483  lttri3  7868  ltleap  8418  mulgt1  8645  nominpos  8981  uzind  9186  indstr  9415  eqreznegel  9433  shftuz  10621  caucvgrelemcau  10784  sqrtsq  10848  mulcn2  11113  dvdsgcdb  11737  algcvgblem  11766  lcmdvdsb  11801  rpexp  11867  cnntr  12433  cnrest2  12444  txlm  12487  metrest  12714  bj-om  13306