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  4359  sotritrieq  4361  ordsucss  4541  ordpwsucss  4604  peano5  4635  iss  4993  funssres  5301  ssimaex  5625  elpreima  5684  resflem  5729  tposfo2  6334  nnmord  6584  map0g  6756  mapsn  6758  enq0tr  7520  addnqprl  7615  addnqpru  7616  cauappcvgprlemdisj  7737  lttri3  8125  ltleap  8678  mulgt1  8909  nominpos  9248  uzind  9456  indstr  9686  eqreznegel  9707  shftuz  11001  caucvgrelemcau  11164  sqrtsq  11228  mulcn2  11496  dvdsgcdb  12207  algcvgblem  12244  lcmdvdsb  12279  rpexp  12348  infpnlem1  12555  imasring  13698  unitmulclb  13748  cnntr  14569  cnrest2  14580  txlm  14623  metrest  14850  bj-om  15691