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  1752  equsexd  1753  rexim  2601  rr19.28v  2915  sotricim  4375  sotritrieq  4377  ordsucss  4557  ordpwsucss  4620  peano5  4651  iss  5011  funssres  5319  ssimaex  5650  elpreima  5709  resflem  5754  tposfo2  6363  nnmord  6613  map0g  6785  mapsn  6787  enq0tr  7560  addnqprl  7655  addnqpru  7656  cauappcvgprlemdisj  7777  lttri3  8165  ltleap  8718  mulgt1  8949  nominpos  9288  uzind  9497  indstr  9727  eqreznegel  9748  shftuz  11178  caucvgrelemcau  11341  sqrtsq  11405  mulcn2  11673  dvdsgcdb  12384  algcvgblem  12421  lcmdvdsb  12456  rpexp  12525  infpnlem1  12732  imasring  13876  unitmulclb  13926  cnntr  14747  cnrest2  14758  txlm  14801  metrest  15028  bj-om  15987