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  8924  mulgt1  9157  nominpos  9496  uzind  9710  indstr  9946  eqreznegel  9967  ccatopth  11436  shftuz  11530  caucvgrelemcau  11694  sqrtsq  11758  mulcn2  12026  dvdsgcdb  12738  algcvgblem  12775  lcmdvdsb  12810  rpexp  12879  infpnlem1  13086  imasring  14311  unitmulclb  14363  cnntr  15220  cnrest2  15231  txlm  15274  metrest  15501  uspgr2wlkeq  16490  bj-om  16847