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  1778  rexim  2638  rr19.28v  2960  sotricim  4449  sotritrieq  4451  ordsucss  4631  ordpwsucss  4694  peano5  4725  iss  5089  funssres  5400  ssimaex  5743  elpreima  5802  resflem  5846  tposfo2  6511  nnmord  6763  map0g  6935  mapsn  6938  enq0tr  7765  addnqprl  7860  addnqpru  7861  cauappcvgprlemdisj  7982  lttri3  8369  ltleap  8923  mulgt1  9154  nominpos  9493  uzind  9707  indstr  9943  eqreznegel  9964  ccatopth  11433  shftuz  11527  caucvgrelemcau  11690  sqrtsq  11754  mulcn2  12022  dvdsgcdb  12734  algcvgblem  12771  lcmdvdsb  12806  rpexp  12875  infpnlem1  13082  imasring  14292  unitmulclb  14344  cnntr  15202  cnrest2  15213  txlm  15256  metrest  15483  uspgr2wlkeq  16472  bj-om  16819