Theorem 3adant3 1048

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 1025	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜃) → (𝜑 ∧ 𝜓))
2		3adant.1	. 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
3	1, 2	syl 14	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜃) → 𝜒)

This proof depends on syntax axioms:   → wi 4   ∧ wa 104   ∧ w3a 1009

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106

This proof depends on definitions:  df-bi 117  df-3an 1011

This theorem is used by:  stoic4a  1481  stoic4b  1482  vtoclgft  2873  eqeu  2996  ssprsseq  3877  tpssi  3884  issod  4464  sotricim  4468  soinxp  4845  funopg  5411  fnco  5491  resasplitss  5569  resdif  5661  fnimapr  5763  ftpg  5899  fsnunfv  5916  fvpr1g  5921  fvpr2g  5922  f1ocnvfvb  5986  f1oiso2  6033  moriotass  6069  f1ofveu  6073  acexmid  6084  ovig  6210  ov6g  6227  ovg  6228  ot1stg  6386  ot2ndg  6387  poxp  6468  suppvalfn  6481  suppsnopdc  6490  suppfnss  6497  funsssuppss  6498  brtposg  6525  smores3  6564  smoiso  6573  rdgivallem  6652  frecsuclem  6677  nnaord  6782  nnaword  6784  nnawordex  6802  ecopovtrn  6906  ecopovtrng  6909  xpdom3m  7132  mapxpen  7148  sbthlemi4  7277  djuenun  7568  netap  7620  2omotaplemap  7623  ltsopi  7687  addcanpig  7701  distrnqg  7754  ltsonq  7765  ltanqg  7767  ltmnqg  7768  nnanq0  7825  distrnq0  7826  distnq0r  7830  prarloclem  7868  genpassl  7891  genpassu  7892  distrlem1prl  7949  distrlem1pru  7950  distrlem5prl  7953  distrlem5pru  7954  1idprl  7957  1idpru  7958  ltpopr  7962  ltsopr  7963  ltexprlemm  7967  ltexprlemfl  7976  ltexprlemfu  7978  addcanprlemu  7982  recexprlem1ssl  8000  recexprlem1ssu  8001  aptipr  8008  lttrsr  8129  ltsosr  8131  ltasrg  8137  recexgt0sr  8140  mulextsr1  8148  axmulass  8240  ltxrlt  8391  axltwlin  8393  axlttrn  8394  axltadd  8395  letr  8408  mul12  8456  add12  8485  subadd  8530  addsub  8538  npncan  8548  nppcan  8549  nnpcan  8550  nppcan3  8551  pnpcan  8566  pnncan  8568  ppncan  8569  subdi  8713  ltaddsub2  8766  leaddsub2  8768  ltaddsublt  8901  apreap  8917  lemul1  8923  reapmul1lem  8924  reapadd1  8926  reapcotr  8928  receuap  9001  divassap  9022  div23ap  9023  divmulassap  9027  divmulasscomap  9028  divcanap4  9031  divsubdirap  9040  divcanap5  9046  divdiv32ap  9052  divdivap2  9056  div2subap  9169  letrp1  9180  ltmulgt12  9197  lediv1  9201  ltdiv2  9219  lediv2  9223  lbinfle  9282  indfdc  9300  indfval  9301  difgtsumgt  9718  xrletr  10220  xrre2  10233  xaddass  10281  ixxdisj  10315  ubioc1  10341  lbico1  10342  elioo5  10345  iccsupr  10378  lbicc2  10396  ubicc2  10397  iccneg  10401  icoshft  10402  icodisj  10404  lincmble  10416  iccf1o  10417  iccen  10419  zltaddlt1le  10420  fztri3or  10453  fzdcel  10454  fzen  10457  uzsubsubfz  10462  fzrevral2  10523  fzshftral  10525  fz0fzdiffz0  10547  difelfznle  10552  fzo1fzo0n0  10605  fzonmapblen  10609  fzosubel2  10623  ubmelfzo  10628  elfzodifsumelfzo  10629  ssfzo12bi  10653  ubmelm1fzo  10654  subfzo0  10671  ceiqle  10763  modqid2  10801  zmodidfzoimp  10804  addmodidr  10823  modfzo0difsn  10845  addmodlteq  10848  frec2uzf1od  10856  exprecap  11030  expdivap  11040  expubnd  11046  sqdivap  11053  mulbinom2  11106  bernneq2  11112  mulsubdivbinom2ap  11163  bcval3  11203  bccmpl  11206  omgadd  11256  ccatval1  11379  ccatval2  11380  ccatass  11390  lswccatn0lsw  11393  ccatws1lenp1bg  11417  ccatw2s1leng  11420  pfxfv  11470  pfxnd  11475  pfxtrcfv  11479  pfxsuffeqwrdeq  11484  swrdswrd  11491  pfxpfx  11494  ccatopth2  11503  pfxccatin12lem4  11512  pfxccatin12lem1  11514  pfxccatin12lem2  11517  pfxccatin12lem3  11518  pfxccatin12  11519  pfxccat3  11520  swrdccat  11521  pfxccatpfx1  11522  pfxccatpfx2  11523  s3fv0g  11577  s3fv1g  11578  s3fv2g  11579  shftval2  11605  mulreap  11643  elicc4abs  11875  abssubge0  11883  abssuble0  11884  maxleast  11994  maxltsup  11999  xrmaxltsup  12040  xrmineqinf  12051  xrltmininf  12052  xrlemininf  12053  fsumdifsnconst  12238  prodfap0  12328  prodfrecap  12329  fprodabs  12399  sin01gt0  12545  cos01gt0  12546  sin02gt0  12547  dvdscmul  12601  summodnegmod  12605  modmulconst  12606  dvdsleabs  12628  dvdsleabs2  12629  addmodlteqALT  12642  dvdsexp  12644  mulmoddvds  12646  divalgb  12708  divgcdz  12764  gcdass  12808  mulgcdr  12811  gcddiv  12812  uzwodc  12830  lcmass  12879  coprmdvds  12886  qredeq  12890  qredeu  12891  congr  12894  divgcdcoprm0  12895  divgcdcoprmex  12896  cncongr1  12897  cncongr2  12898  isprm3  12912  dvdsnprmd  12919  euclemma  12941  prmdvdsexpb  12944  prmexpb  12946  rpexp  12948  znege1  12974  modprminv  13048  modprminveq  13049  vfermltl  13050  modprm0  13053  modprmn0modprm0  13055  coprimeprodsq  13056  coprimeprodsq2  13057  pythagtriplem1  13064  pythagtriplem3  13066  pythagtriplem6  13069  pythagtriplem12  13074  pythagtriplem13  13075  pythagtriplem14  13076  pythagtriplem16  13078  pythagtriplem19  13081  pythagtrip  13082  pcmul  13100  pcdiv  13101  pcqcl  13105  pcgcd1  13127  pcgcd  13128  dvdsprmpweq  13134  difsqpwdvds  13137  pcfaclem  13148  ballotfilemsgt1  13303  ballotfilemrv1  13313  ballotfilemrv2  13314  ballotfilemfrcn0  13322  unbendc  13394  strle3g  13511  ercpbl  13701  grpinvid1  13906  grpinvid2  13907  grpasscan1  13917  grpasscan2  13918  grpidrcan  13919  grpidlcan  13920  grpinvadd  13932  grpsubadd  13942  grppncan  13945  qussub  14089  subcmnd  14186  pwsinvg  14264  rng1zrlem  14307  mulgass2  14412  dvrcan1  14496  dvrcan3  14497  rmodislmodlem  14736  rmodislmod  14737  islssm  14743  lsselg  14747  lspss  14785  lspssp  14789  lsslsp  14815  islidlm  14865  lidlnegcl  14871  lidlsubcl  14873  zndvds  15033  assa2ass  15058  assa2ass2  15059  aspss  15068  basgen  15230  clsss  15268  ntrin  15274  ntrcls0  15281  neiint  15295  neiss  15300  neipsm  15304  opnssneib  15306  innei  15313  restco  15324  iscnp  15349  cnconst2  15383  txcn  15425  psmetsym  15479  psmetlecl  15484  distspace  15485  xmetlecl  15517  xmetsym  15518  xblcntrps  15563  xblcntr  15564  blssec  15588  blpnfctr  15589  txmetcn  15669  cnmet  15680  dvid  15845  dvidre  15847  dvply1  15915  ptolemy  15975  sinq12gt0  15981  sincosq1eq  15990  rpcxpsub  16063  relogbexpap  16113  logbleb  16116  logblt  16117  rplogbcxp  16118  lgsval4  16237  lgsmod  16243  lgsne0  16255  lgsmulsqcoprm  16263  2lgsoddprmlem1  16322  structiedg0val  16379  lpvtx  16418  upgredg2vtx  16487  upgredgpr  16488  ushgredgedg  16565  ushgredgedgloop  16567  usgr2v1e2w  16585  wlkeq  16693  clwwlkccatlem  16739  clwwlkccat  16740  clwwlkext2edg  16761  clwwlknccat  16762  s2elclwwlknon2  16775  clwwlknonex2lem2  16777  repiecele0  17173  repiecege0  17174