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 ⊢ (𝜑 → (𝜓 → (𝜒 ∧ 𝜃)))

This proof depends on syntax axioms:   → wi 4   ∧ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 108

This theorem is used by:  jca2  308  jctild  316  jctird  317  ancld  325  ancrd  326  anim12ii  343  equsex  1780  equsexd  1782  rexim  2644  rr19.28v  2966  sotricim  4468  sotritrieq  4470  ordsucss  4651  ordpwsucss  4714  peano5  4745  iss  5109  funssres  5420  ssimaex  5764  elpreima  5828  resflem  5872  tposfo2  6538  nnmord  6790  map0g  6969  mapsn  6972  enq0tr  7802  addnqprl  7897  addnqpru  7898  cauappcvgprlemdisj  8019  lttri3  8406  ltleap  8963  mulgt1  9196  nominpos  9548  uzind  9762  indstr  10003  eqreznegel  10024  ccatopth  11503  shftuz  11597  caucvgrelemcau  11761  sqrtsq  11825  mulcn2  12096  dvdsgcdb  12808  algcvgblem  12845  lcmdvdsb  12880  rpexp  12950  infpnlem1  13160  imasring  14420  unitmulclb  14472  assapropd  15065  cnntr  15378  cnrest2  15389  txlm  15432  metrest  15659  uspgr2wlkeq  16728  bj-om  17085