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  1708  equsexd  1709  rexim  2551  rr19.28v  2852  sotricim  4282  sotritrieq  4284  ordsucss  4461  ordpwsucss  4524  peano5  4555  iss  4909  funssres  5209  ssimaex  5526  elpreima  5583  resflem  5628  tposfo2  6208  nnmord  6457  map0g  6626  mapsn  6628  enq0tr  7337  addnqprl  7432  addnqpru  7433  cauappcvgprlemdisj  7554  lttri3  7940  ltleap  8490  mulgt1  8717  nominpos  9053  uzind  9258  indstr  9487  eqreznegel  9505  shftuz  10699  caucvgrelemcau  10862  sqrtsq  10926  mulcn2  11191  dvdsgcdb  11877  algcvgblem  11906  lcmdvdsb  11941  rpexp  12007  cnntr  12585  cnrest2  12596  txlm  12639  metrest  12866  bj-om  13472