Theorem 3adant3 1041

Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 16-Jul-1995.)

Hypothesis

Ref	Expression
3adant.1	⊢ ((𝜑 ∧ 𝜓) → 𝜒)

Assertion

Ref	Expression
3adant3	⊢ ((𝜑 ∧ 𝜓 ∧ 𝜃) → 𝜒)

Proof of Theorem 3adant3

Step	Hyp	Ref	Expression
1		3simpa 1018	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜃) → (𝜑 ∧ 𝜓))
2		3adant.1	. 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
3	1, 2	syl 14	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜃) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 104   ∧ w3a 1002

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106

This theorem depends on definitions:  df-bi 117  df-3an 1004

This theorem is referenced by:  stoic4a  1474  stoic4b  1475  vtoclgft  2852  eqeu  2974  ssprsseq  3833  tpssi  3840  issod  4414  sotricim  4418  soinxp  4794  funopg  5358  fnco  5437  resasplitss  5513  resdif  5602  fnimapr  5702  ftpg  5833  fsnunfv  5850  fvpr1g  5855  fvpr2g  5856  f1ocnvfvb  5916  f1oiso2  5963  moriotass  5997  f1ofveu  6001  acexmid  6012  ovig  6138  ov6g  6155  ovg  6156  ot1stg  6310  ot2ndg  6311  poxp  6392  brtposg  6415  smores3  6454  smoiso  6463  rdgivallem  6542  frecsuclem  6567  nnaord  6672  nnaword  6674  nnawordex  6692  ecopovtrn  6796  ecopovtrng  6799  xpdom3m  7013  mapxpen  7029  sbthlemi4  7150  djuenun  7417  netap  7463  2omotaplemap  7466  ltsopi  7530  addcanpig  7544  distrnqg  7597  ltsonq  7608  ltanqg  7610  ltmnqg  7611  nnanq0  7668  distrnq0  7669  distnq0r  7673  prarloclem  7711  genpassl  7734  genpassu  7735  distrlem1prl  7792  distrlem1pru  7793  distrlem5prl  7796  distrlem5pru  7797  1idprl  7800  1idpru  7801  ltpopr  7805  ltsopr  7806  ltexprlemm  7810  ltexprlemfl  7819  ltexprlemfu  7821  addcanprlemu  7825  recexprlem1ssl  7843  recexprlem1ssu  7844  aptipr  7851  lttrsr  7972  ltsosr  7974  ltasrg  7980  recexgt0sr  7983  mulextsr1  7991  axmulass  8083  ltxrlt  8235  axltwlin  8237  axlttrn  8238  axltadd  8239  letr  8252  mul12  8298  add12  8327  subadd  8372  addsub  8380  npncan  8390  nppcan  8391  nnpcan  8392  nppcan3  8393  pnpcan  8408  pnncan  8410  ppncan  8411  subdi  8554  ltaddsub2  8607  leaddsub2  8609  ltaddsublt  8741  apreap  8757  lemul1  8763  reapmul1lem  8764  reapadd1  8766  reapcotr  8768  receuap  8839  divassap  8860  div23ap  8861  divmulassap  8865  divmulasscomap  8866  divcanap4  8869  divsubdirap  8878  divcanap5  8884  divdiv32ap  8890  divdivap2  8894  div2subap  9007  letrp1  9018  ltmulgt12  9035  lediv1  9039  ltdiv2  9057  lediv2  9061  lbinfle  9120  difgtsumgt  9539  xrletr  10033  xrre2  10046  xaddass  10094  ixxdisj  10128  ubioc1  10154  lbico1  10155  elioo5  10158  iccsupr  10191  lbicc2  10209  ubicc2  10210  iccneg  10214  icoshft  10215  icodisj  10217  iccf1o  10229  iccen  10231  zltaddlt1le  10232  fztri3or  10264  fzdcel  10265  fzen  10268  uzsubsubfz  10272  fzrevral2  10331  fzshftral  10333  fz0fzdiffz0  10355  difelfznle  10360  fzo1fzo0n0  10412  fzonmapblen  10416  fzosubel2  10430  ubmelfzo  10435  elfzodifsumelfzo  10436  ssfzo12bi  10460  ubmelm1fzo  10461  subfzo0  10478  ceiqle  10565  modqid2  10603  zmodidfzoimp  10606  addmodidr  10625  modfzo0difsn  10647  addmodlteq  10650  frec2uzf1od  10658  exprecap  10832  expdivap  10842  expubnd  10848  sqdivap  10855  mulbinom2  10908  bernneq2  10913  mulsubdivbinom2ap  10963  bcval3  11003  bccmpl  11006  omgadd  11055  ccatval1  11164  ccatval2  11165  ccatass  11175  lswccatn0lsw  11178  ccatws1lenp1bg  11202  ccatw2s1leng  11205  pfxfv  11255  pfxnd  11260  pfxtrcfv  11264  pfxsuffeqwrdeq  11269  swrdswrd  11276  pfxpfx  11279  ccatopth2  11288  pfxccatin12lem4  11297  pfxccatin12lem1  11299  pfxccatin12lem2  11302  pfxccatin12lem3  11303  pfxccatin12  11304  pfxccat3  11305  swrdccat  11306  pfxccatpfx1  11307  pfxccatpfx2  11308  s3fv0g  11362  s3fv1g  11363  s3fv2g  11364  shftval2  11377  mulreap  11415  elicc4abs  11645  abssubge0  11653  abssuble0  11654  maxleast  11764  maxltsup  11769  xrmaxltsup  11809  xrmineqinf  11820  xrltmininf  11821  xrlemininf  11822  fsumdifsnconst  12006  prodfap0  12096  prodfrecap  12097  fprodabs  12167  sin01gt0  12313  cos01gt0  12314  sin02gt0  12315  dvdscmul  12369  summodnegmod  12373  modmulconst  12374  dvdsleabs  12396  dvdsleabs2  12397  addmodlteqALT  12410  dvdsexp  12412  mulmoddvds  12414  divalgb  12476  divgcdz  12532  gcdass  12576  mulgcdr  12579  gcddiv  12580  uzwodc  12598  lcmass  12647  coprmdvds  12654  qredeq  12658  qredeu  12659  congr  12662  divgcdcoprm0  12663  divgcdcoprmex  12664  cncongr1  12665  cncongr2  12666  isprm3  12680  dvdsnprmd  12687  euclemma  12708  prmdvdsexpb  12711  prmexpb  12713  rpexp  12715  znege1  12740  modprminv  12812  modprminveq  12813  vfermltl  12814  modprm0  12817  modprmn0modprm0  12819  coprimeprodsq  12820  coprimeprodsq2  12821  pythagtriplem1  12828  pythagtriplem3  12830  pythagtriplem6  12833  pythagtriplem12  12838  pythagtriplem13  12839  pythagtriplem14  12840  pythagtriplem16  12842  pythagtriplem19  12845  pythagtrip  12846  pcmul  12864  pcdiv  12865  pcqcl  12869  pcgcd1  12891  pcgcd  12892  dvdsprmpweq  12898  difsqpwdvds  12901  pcfaclem  12912  unbendc  13065  strle3g  13181  ercpbl  13404  grpinvid1  13625  grpinvid2  13626  grpasscan1  13636  grpasscan2  13637  grpidrcan  13638  grpidlcan  13639  grpinvadd  13651  grpsubadd  13661  grppncan  13664  pwsinvg  13685  qussub  13814  subcmnd  13910  mulgass2  14061  dvrcan1  14144  dvrcan3  14145  rmodislmodlem  14354  rmodislmod  14355  islssm  14361  lsselg  14365  lspss  14403  lspssp  14407  lsslsp  14433  islidlm  14483  lidlnegcl  14489  lidlsubcl  14491  zndvds  14653  basgen  14794  clsss  14832  ntrin  14838  ntrcls0  14845  neiint  14859  neiss  14864  neipsm  14868  opnssneib  14870  innei  14877  restco  14888  iscnp  14913  cnconst2  14947  txcn  14989  psmetsym  15043  psmetlecl  15048  distspace  15049  xmetlecl  15081  xmetsym  15082  xblcntrps  15127  xblcntr  15128  blssec  15152  blpnfctr  15153  txmetcn  15233  cnmet  15244  dvid  15409  dvidre  15411  dvply1  15479  ptolemy  15538  sinq12gt0  15544  sincosq1eq  15553  rpcxpsub  15622  relogbexpap  15672  logbleb  15675  logblt  15676  rplogbcxp  15677  lgsval4  15739  lgsmod  15745  lgsne0  15757  lgsmulsqcoprm  15765  2lgsoddprmlem1  15824  structiedg0val  15881  lpvtx  15920  upgredg2vtx  15987  upgredgpr  15988  ushgredgedg  16065  ushgredgedgloop  16067  usgr2v1e2w  16085  wlkeq  16151  clwwlkccatlem  16195  clwwlkccat  16196  clwwlkext2edg  16217  clwwlknccat  16218  s2elclwwlknon2  16231  clwwlknonex2lem2  16233