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  1776  equsexd  1777  rexim  2627  rr19.28v  2947  sotricim  4426  sotritrieq  4428  ordsucss  4608  ordpwsucss  4671  peano5  4702  iss  5065  funssres  5376  ssimaex  5716  elpreima  5775  resflem  5819  tposfo2  6476  nnmord  6728  map0g  6900  mapsn  6902  enq0tr  7697  addnqprl  7792  addnqpru  7793  cauappcvgprlemdisj  7914  lttri3  8302  ltleap  8855  mulgt1  9086  nominpos  9425  uzind  9634  indstr  9870  eqreznegel  9891  ccatopth  11344  shftuz  11438  caucvgrelemcau  11601  sqrtsq  11665  mulcn2  11933  dvdsgcdb  12645  algcvgblem  12682  lcmdvdsb  12717  rpexp  12786  infpnlem1  12993  imasring  14139  unitmulclb  14190  cnntr  15016  cnrest2  15027  txlm  15070  metrest  15297  uspgr2wlkeq  16286  bj-om  16633