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  1728  equsexd  1729  rexim  2571  rr19.28v  2878  sotricim  4324  sotritrieq  4326  ordsucss  4504  ordpwsucss  4567  peano5  4598  iss  4954  funssres  5259  ssimaex  5578  elpreima  5636  resflem  5681  tposfo2  6268  nnmord  6518  map0g  6688  mapsn  6690  enq0tr  7433  addnqprl  7528  addnqpru  7529  cauappcvgprlemdisj  7650  lttri3  8037  ltleap  8589  mulgt1  8820  nominpos  9156  uzind  9364  indstr  9593  eqreznegel  9614  shftuz  10826  caucvgrelemcau  10989  sqrtsq  11053  mulcn2  11320  dvdsgcdb  12014  algcvgblem  12049  lcmdvdsb  12084  rpexp  12153  infpnlem1  12357  unitmulclb  13283  cnntr  13728  cnrest2  13739  txlm  13782  metrest  14009  bj-om  14692