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  1742  equsexd  1743  rexim  2591  rr19.28v  2904  sotricim  4358  sotritrieq  4360  ordsucss  4540  ordpwsucss  4603  peano5  4634  iss  4992  funssres  5300  ssimaex  5622  elpreima  5681  resflem  5726  tposfo2  6325  nnmord  6575  map0g  6747  mapsn  6749  enq0tr  7501  addnqprl  7596  addnqpru  7597  cauappcvgprlemdisj  7718  lttri3  8106  ltleap  8659  mulgt1  8890  nominpos  9229  uzind  9437  indstr  9667  eqreznegel  9688  shftuz  10982  caucvgrelemcau  11145  sqrtsq  11209  mulcn2  11477  dvdsgcdb  12180  algcvgblem  12217  lcmdvdsb  12252  rpexp  12321  infpnlem1  12528  imasring  13620  unitmulclb  13670  cnntr  14461  cnrest2  14472  txlm  14515  metrest  14742  bj-om  15583