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  7801  addnqprl  7896  addnqpru  7897  cauappcvgprlemdisj  8018  lttri3  8405  ltleap  8961  mulgt1  9194  nominpos  9545  uzind  9759  indstr  9995  eqreznegel  10016  ccatopth  11490  shftuz  11584  caucvgrelemcau  11748  sqrtsq  11812  mulcn2  12080  dvdsgcdb  12792  algcvgblem  12829  lcmdvdsb  12864  rpexp  12933  infpnlem1  13140  imasring  14371  unitmulclb  14423  assapropd  15016  cnntr  15328  cnrest2  15339  txlm  15382  metrest  15609  uspgr2wlkeq  16618  bj-om  16975