Theorem jcad 516

Description: Deduction conjoining the consequents of two implications. Deduction form of jca 515 and double deduction form of pm3.2 473 and pm3.2i 474. (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 473	. 2 ⊢ (𝜒 → (𝜃 → (𝜒 ∧ 𝜃)))
4	1, 2, 3	syl6c 70	1 ⊢ (𝜑 → (𝜓 → (𝜒 ∧ 𝜃)))

Syntax hints:   → wi 4   ∧ wa 399

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 210  df-an 400

This theorem is referenced by:  jca2  517  jctild  529  jctird  530  ancld  554  ancrd  555  oplem1  1052  2eu1  2712  2eu1v  2713  disjxiun  5027  iss  5870  oneqmini  6210  funssres  6368  elpreima  6805  isomin  7069  oneqmin  7500  frxp  7803  tposfo2  7898  oa00  8168  odi  8188  oneo  8190  oeordsuc  8203  oelim2  8204  nnarcl  8225  nnmord  8241  nnneo  8261  map0g  8431  onomeneq  8693  pssnn  8720  fodomfib  8782  inf3lem4  9078  cplem1  9302  karden  9308  alephordi  9485  cardinfima  9508  dfac5lem5  9538  isf34lem4  9788  axcc4  9850  axdc3lem2  9862  zorn2lem4  9910  zorn2lem7  9913  indpi  10318  genpcl  10419  addclprlem2  10428  ltaddpr  10445  ltexprlem5  10451  suplem1pr  10463  ltlen  10730  dedekind  10792  mulgt1  11488  sup2  11584  nominpos  11862  uzind  12062  xrmaxlt  12562  xrltmin  12563  xrmaxle  12564  xrlemin  12565  xmullem2  12646  ccatopth  14069  shftuz  14420  sqreulem  14711  limsupbnd2  14832  mulcn2  14944  sadcaddlem  15796  dvdsgcdb  15883  algcvgblem  15911  lcmdvdsb  15947  rpexp  16054  infpnlem1  16236  divsfval  16812  iscatd  16936  posasymb  17554  plttr  17572  joinle  17616  meetle  17630  latnlej  17670  latnlej2  17673  lsmlub  18782  imasring  19365  unitmulclb  19411  lbspss  19847  lspsneu  19888  lspprat  19918  assapropd  20558  isclo2  21693  cncls2  21878  cncls  21879  cnntr  21880  cnrest2  21891  cmpsub  22005  cmpcld  22007  kgenss  22148  ptpjpre1  22176  txlm  22253  qtoptop2  22304  cmphaushmeo  22405  fbun  22445  isfild  22463  fbasrn  22489  fgtr  22495  ufinffr  22534  rnelfm  22558  fmfnfmlem4  22562  ghmcnp  22720  metrest  23131  icoopnst  23544  iocopnst  23545  dgreq0  24862  plyexmo  24909  cxpeq0  25269  mumullem2  25765  chpchtsum  25803  bposlem7  25874  lgsqr  25935  uspgr2wlkeq  27435  wwlknllvtx  27632  ex-natded5.3-2  28193  ubthlem1  28653  axhcompl-zf  28781  ococss  29076  nmopun  29797  elpjrn  29973  stm1addi  30028  stm1add3i  30030  mdsl1i  30104  chrelat2i  30148  atexch  30164  atcvat4i  30180  mdsymlem3  30188  bian1d  30230  bnj600  32301  subgrwlk  32492  pthacycspth  32517  subfacval2  32547  climuzcnv  33027  fundmpss  33122  soseq  33209  sltres  33282  nosupno  33316  segconeq  33584  ifscgr  33618  endofsegid  33659  colinbtwnle  33692  trer  33777  ivthALT  33796  fnessref  33818  fnemeet2  33828  fnejoin2  33830  onsuct0  33902  bj-ideqg1  34579  bj-elid6  34585  bj-finsumval0  34700  bj-isrvec2  34714  bj-bary1  34726  icorempo  34768  isbasisrelowllem1  34772  isbasisrelowllem2  34773  relowlpssretop  34781  finxpsuclem  34814  pibt2  34834  poimirlem31  35088  isbnd2  35221  bfplem2  35261  ghomco  35329  cnf1dd  35528  contrd  35535  mpobi123f  35600  mptbi12f  35604  iss2  35761  jca2r  36151  prter2  36177  lshpset2N  36415  cvrnbtwn2  36571  cvrnbtwn3  36572  cvrnbtwn4  36575  cvlcvr1  36635  hlrelat2  36699  cvrat4  36739  islpln2a  36844  linepsubN  37048  elpaddn0  37096  paddssw2  37140  pmapjoin  37148  ispsubcl2N  37243  dochkrshp  38682  dochsatshp  38747  mapdh9a  39085  hdmap11lem2  39138  frlmfzowrdb  39438  sn-sup2  39594  pwinfi3  40262  clsk1independent  40749  gneispace  40837  pm11.71  41101  2reu8i  43669  sbgoldbaltlem2  44298  setrec1lem4  45220