Theorem jcad 514

Description: Deduction conjoining the consequents of two implications. Deduction form of jca 513 and double deduction form of pm3.2 471 and pm3.2i 472. (Contributed by NM, 15-Jul-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 471	. 2 ⊢ (𝜒 → (𝜃 → (𝜒 ∧ 𝜃)))
4	1, 2, 3	syl6c 70	1 ⊢ (𝜑 → (𝜓 → (𝜒 ∧ 𝜃)))

Syntax hints:   → wi 4   ∧ wa 397

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 206  df-an 398

This theorem is referenced by:  jca2  515  jctild  527  jctird  528  ancld  552  ancrd  553  oplem1  1056  2eu1  2647  2eu1v  2648  disjxiun  5145  iss  6034  oneqmini  6414  funssres  6590  elpreima  7057  isomin  7331  oneqmin  7785  frxp  8109  soseq  8142  tposfo2  8231  oa00  8556  odi  8576  oneo  8578  oeordsuc  8591  oelim2  8592  nnarcl  8613  nnmord  8629  nnneo  8651  map0g  8875  pssnn  9165  onomeneqOLD  9226  pssnnOLD  9262  fodomfib  9323  inf3lem4  9623  cplem1  9881  karden  9887  alephordi  10066  cardinfima  10089  dfac5lem5  10119  isf34lem4  10369  axcc4  10431  axdc3lem2  10443  zorn2lem4  10491  zorn2lem7  10494  indpi  10899  genpcl  11000  addclprlem2  11009  ltaddpr  11026  ltexprlem5  11032  suplem1pr  11044  ltlen  11312  dedekind  11374  mulgt1  12070  sup2  12167  nominpos  12446  uzind  12651  xrmaxlt  13157  xrltmin  13158  xrmaxle  13159  xrlemin  13160  xmullem2  13241  ccatopth  14663  shftuz  15013  sqreulem  15303  limsupbnd2  15424  mulcn2  15537  sadcaddlem  16395  dvdsgcdb  16484  algcvgblem  16511  lcmdvdsb  16547  rpexp  16656  infpnlem1  16840  divsfval  17490  iscatd  17614  posasymb  18269  plttr  18292  joinle  18336  meetle  18350  latnlej  18406  latnlej2  18409  lsmlub  19527  imasring  20137  unitmulclb  20188  lbspss  20686  lspsneu  20729  lspprat  20759  assapropd  21418  isclo2  22584  cncls2  22769  cncls  22770  cnntr  22771  cnrest2  22782  cmpsub  22896  cmpcld  22898  kgenss  23039  ptpjpre1  23067  txlm  23144  qtoptop2  23195  cmphaushmeo  23296  fbun  23336  isfild  23354  fbasrn  23380  fgtr  23386  ufinffr  23425  rnelfm  23449  fmfnfmlem4  23453  ghmcnp  23611  metrest  24025  icoopnst  24447  iocopnst  24448  dgreq0  25771  plyexmo  25818  cxpeq0  26178  mumullem2  26674  chpchtsum  26712  bposlem7  26783  lgsqr  26844  sltres  27155  nosupno  27196  noinfno  27211  uspgr2wlkeq  28893  wwlknllvtx  29090  ex-natded5.3-2  29651  ubthlem1  30111  axhcompl-zf  30239  ococss  30534  nmopun  31255  elpjrn  31431  stm1addi  31486  stm1add3i  31488  mdsl1i  31562  chrelat2i  31606  atexch  31622  atcvat4i  31638  mdsymlem3  31646  bian1d  31688  bnj600  33919  subgrwlk  34112  pthacycspth  34137  subfacval2  34167  climuzcnv  34645  fundmpss  34727  segconeq  34971  ifscgr  35005  endofsegid  35046  colinbtwnle  35079  gg-dvfsumlem2  35172  trer  35190  ivthALT  35209  fnessref  35231  fnemeet2  35241  fnejoin2  35243  onsuct0  35315  bj-ideqg1  36034  bj-elid6  36040  bj-finsumval0  36155  bj-isrvec2  36170  bj-bary1  36182  icorempo  36221  isbasisrelowllem1  36225  isbasisrelowllem2  36226  relowlpssretop  36234  finxpsuclem  36267  pibt2  36287  poimirlem31  36508  isbnd2  36640  bfplem2  36680  ghomco  36748  cnf1dd  36947  contrd  36954  mpobi123f  37019  mptbi12f  37023  iss2  37202  refressn  37302  jca2r  37714  prter2  37740  lshpset2N  37978  cvrnbtwn2  38134  cvrnbtwn3  38135  cvrnbtwn4  38138  cvlcvr1  38198  hlrelat2  38263  cvrat4  38303  islpln2a  38408  linepsubN  38612  elpaddn0  38660  paddssw2  38704  pmapjoin  38712  ispsubcl2N  38807  dochkrshp  40246  dochsatshp  40311  mapdh9a  40649  hdmap11lem2  40702  frlmfzowrdb  41076  sn-sup2  41339  pwinfi3  42300  clsk1independent  42783  gneispace  42871  pm11.71  43142  tworepnotupword  45587  2reu8i  45808  sbgoldbaltlem2  46435  setrec1lem4  47689