Theorem 3adant3 1044

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

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

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 1007

This theorem is referenced by:  stoic4a  1477  stoic4b  1478  vtoclgft  2865  eqeu  2987  ssprsseq  3856  tpssi  3863  issod  4440  sotricim  4444  soinxp  4820  funopg  5386  fnco  5466  resasplitss  5544  resdif  5636  fnimapr  5737  ftpg  5868  fsnunfv  5885  fvpr1g  5890  fvpr2g  5891  f1ocnvfvb  5953  f1oiso2  6000  moriotass  6034  f1ofveu  6038  acexmid  6049  ovig  6175  ov6g  6192  ovg  6193  ot1stg  6346  ot2ndg  6347  poxp  6428  suppvalfn  6441  suppsnopdc  6450  suppfnss  6457  funsssuppss  6458  brtposg  6485  smores3  6524  smoiso  6533  rdgivallem  6612  frecsuclem  6637  nnaord  6742  nnaword  6744  nnawordex  6762  ecopovtrn  6866  ecopovtrng  6869  xpdom3m  7085  mapxpen  7101  sbthlemi4  7230  djuenun  7519  netap  7568  2omotaplemap  7571  ltsopi  7635  addcanpig  7649  distrnqg  7702  ltsonq  7713  ltanqg  7715  ltmnqg  7716  nnanq0  7773  distrnq0  7774  distnq0r  7778  prarloclem  7816  genpassl  7839  genpassu  7840  distrlem1prl  7897  distrlem1pru  7898  distrlem5prl  7901  distrlem5pru  7902  1idprl  7905  1idpru  7906  ltpopr  7910  ltsopr  7911  ltexprlemm  7915  ltexprlemfl  7924  ltexprlemfu  7926  addcanprlemu  7930  recexprlem1ssl  7948  recexprlem1ssu  7949  aptipr  7956  lttrsr  8077  ltsosr  8079  ltasrg  8085  recexgt0sr  8088  mulextsr1  8096  axmulass  8188  ltxrlt  8339  axltwlin  8341  axlttrn  8342  axltadd  8343  letr  8356  mul12  8402  add12  8431  subadd  8476  addsub  8484  npncan  8494  nppcan  8495  nnpcan  8496  nppcan3  8497  pnpcan  8512  pnncan  8514  ppncan  8515  subdi  8658  ltaddsub2  8711  leaddsub2  8713  ltaddsublt  8845  apreap  8861  lemul1  8867  reapmul1lem  8868  reapadd1  8870  reapcotr  8872  receuap  8943  divassap  8964  div23ap  8965  divmulassap  8969  divmulasscomap  8970  divcanap4  8973  divsubdirap  8982  divcanap5  8988  divdiv32ap  8994  divdivap2  8998  div2subap  9111  letrp1  9122  ltmulgt12  9139  lediv1  9143  ltdiv2  9161  lediv2  9165  lbinfle  9224  difgtsumgt  9647  xrletr  10141  xrre2  10154  xaddass  10202  ixxdisj  10236  ubioc1  10262  lbico1  10263  elioo5  10266  iccsupr  10299  lbicc2  10317  ubicc2  10318  iccneg  10322  icoshft  10323  icodisj  10325  lincmble  10337  iccf1o  10338  iccen  10340  zltaddlt1le  10341  fztri3or  10373  fzdcel  10374  fzen  10377  uzsubsubfz  10381  fzrevral2  10440  fzshftral  10442  fz0fzdiffz0  10464  difelfznle  10469  fzo1fzo0n0  10522  fzonmapblen  10526  fzosubel2  10540  ubmelfzo  10545  elfzodifsumelfzo  10546  ssfzo12bi  10570  ubmelm1fzo  10571  subfzo0  10588  ceiqle  10675  modqid2  10713  zmodidfzoimp  10716  addmodidr  10735  modfzo0difsn  10757  addmodlteq  10760  frec2uzf1od  10768  exprecap  10942  expdivap  10952  expubnd  10958  sqdivap  10965  mulbinom2  11018  bernneq2  11023  mulsubdivbinom2ap  11073  bcval3  11113  bccmpl  11116  omgadd  11166  ccatval1  11285  ccatval2  11286  ccatass  11296  lswccatn0lsw  11299  ccatws1lenp1bg  11323  ccatw2s1leng  11326  pfxfv  11376  pfxnd  11381  pfxtrcfv  11385  pfxsuffeqwrdeq  11390  swrdswrd  11397  pfxpfx  11400  ccatopth2  11409  pfxccatin12lem4  11418  pfxccatin12lem1  11420  pfxccatin12lem2  11423  pfxccatin12lem3  11424  pfxccatin12  11425  pfxccat3  11426  swrdccat  11427  pfxccatpfx1  11428  pfxccatpfx2  11429  s3fv0g  11483  s3fv1g  11484  s3fv2g  11485  shftval2  11511  mulreap  11549  elicc4abs  11779  abssubge0  11787  abssuble0  11788  maxleast  11898  maxltsup  11903  xrmaxltsup  11943  xrmineqinf  11954  xrltmininf  11955  xrlemininf  11956  fsumdifsnconst  12141  prodfap0  12231  prodfrecap  12232  fprodabs  12302  sin01gt0  12448  cos01gt0  12449  sin02gt0  12450  dvdscmul  12504  summodnegmod  12508  modmulconst  12509  dvdsleabs  12531  dvdsleabs2  12532  addmodlteqALT  12545  dvdsexp  12547  mulmoddvds  12549  divalgb  12611  divgcdz  12667  gcdass  12711  mulgcdr  12714  gcddiv  12715  uzwodc  12733  lcmass  12782  coprmdvds  12789  qredeq  12793  qredeu  12794  congr  12797  divgcdcoprm0  12798  divgcdcoprmex  12799  cncongr1  12800  cncongr2  12801  isprm3  12815  dvdsnprmd  12822  euclemma  12843  prmdvdsexpb  12846  prmexpb  12848  rpexp  12850  znege1  12875  modprminv  12947  modprminveq  12948  vfermltl  12949  modprm0  12952  modprmn0modprm0  12954  coprimeprodsq  12955  coprimeprodsq2  12956  pythagtriplem1  12963  pythagtriplem3  12965  pythagtriplem6  12968  pythagtriplem12  12973  pythagtriplem13  12974  pythagtriplem14  12975  pythagtriplem16  12977  pythagtriplem19  12980  pythagtrip  12981  pcmul  12999  pcdiv  13000  pcqcl  13004  pcgcd1  13026  pcgcd  13027  dvdsprmpweq  13033  difsqpwdvds  13036  pcfaclem  13047  unbendc  13205  strle3g  13321  ercpbl  13544  grpinvid1  13765  grpinvid2  13766  grpasscan1  13776  grpasscan2  13777  grpidrcan  13778  grpidlcan  13779  grpinvadd  13791  grpsubadd  13801  grppncan  13804  pwsinvg  13825  qussub  13954  subcmnd  14050  mulgass2  14202  dvrcan1  14285  dvrcan3  14286  rmodislmodlem  14498  rmodislmod  14499  islssm  14505  lsselg  14509  lspss  14547  lspssp  14551  lsslsp  14577  islidlm  14627  lidlnegcl  14633  lidlsubcl  14635  zndvds  14797  basgen  14945  clsss  14983  ntrin  14989  ntrcls0  14996  neiint  15010  neiss  15015  neipsm  15019  opnssneib  15021  innei  15028  restco  15039  iscnp  15064  cnconst2  15098  txcn  15140  psmetsym  15194  psmetlecl  15199  distspace  15200  xmetlecl  15232  xmetsym  15233  xblcntrps  15278  xblcntr  15279  blssec  15303  blpnfctr  15304  txmetcn  15384  cnmet  15395  dvid  15560  dvidre  15562  dvply1  15630  ptolemy  15689  sinq12gt0  15695  sincosq1eq  15704  rpcxpsub  15773  relogbexpap  15823  logbleb  15826  logblt  15827  rplogbcxp  15828  lgsval4  15893  lgsmod  15899  lgsne0  15911  lgsmulsqcoprm  15919  2lgsoddprmlem1  15978  structiedg0val  16035  lpvtx  16074  upgredg2vtx  16143  upgredgpr  16144  ushgredgedg  16221  ushgredgedgloop  16223  usgr2v1e2w  16241  wlkeq  16349  clwwlkccatlem  16395  clwwlkccat  16396  clwwlkext2edg  16417  clwwlknccat  16418  s2elclwwlknon2  16431  clwwlknonex2lem2  16433  repiecele0  16810  repiecege0  16811