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  2851  eqeu  2973  ssprsseq  3830  tpssi  3837  issod  4410  sotricim  4414  soinxp  4789  funopg  5352  fnco  5431  resasplitss  5507  resdif  5596  fnimapr  5696  ftpg  5827  fsnunfv  5844  fvpr1g  5849  fvpr2g  5850  f1ocnvfvb  5910  f1oiso2  5957  moriotass  5991  f1ofveu  5995  acexmid  6006  ovig  6132  ov6g  6149  ovg  6150  ot1stg  6304  ot2ndg  6305  poxp  6384  brtposg  6406  smores3  6445  smoiso  6454  rdgivallem  6533  frecsuclem  6558  nnaord  6663  nnaword  6665  nnawordex  6683  ecopovtrn  6787  ecopovtrng  6790  xpdom3m  7001  mapxpen  7017  sbthlemi4  7138  djuenun  7405  netap  7451  2omotaplemap  7454  ltsopi  7518  addcanpig  7532  distrnqg  7585  ltsonq  7596  ltanqg  7598  ltmnqg  7599  nnanq0  7656  distrnq0  7657  distnq0r  7661  prarloclem  7699  genpassl  7722  genpassu  7723  distrlem1prl  7780  distrlem1pru  7781  distrlem5prl  7784  distrlem5pru  7785  1idprl  7788  1idpru  7789  ltpopr  7793  ltsopr  7794  ltexprlemm  7798  ltexprlemfl  7807  ltexprlemfu  7809  addcanprlemu  7813  recexprlem1ssl  7831  recexprlem1ssu  7832  aptipr  7839  lttrsr  7960  ltsosr  7962  ltasrg  7968  recexgt0sr  7971  mulextsr1  7979  axmulass  8071  ltxrlt  8223  axltwlin  8225  axlttrn  8226  axltadd  8227  letr  8240  mul12  8286  add12  8315  subadd  8360  addsub  8368  npncan  8378  nppcan  8379  nnpcan  8380  nppcan3  8381  pnpcan  8396  pnncan  8398  ppncan  8399  subdi  8542  ltaddsub2  8595  leaddsub2  8597  ltaddsublt  8729  apreap  8745  lemul1  8751  reapmul1lem  8752  reapadd1  8754  reapcotr  8756  receuap  8827  divassap  8848  div23ap  8849  divmulassap  8853  divmulasscomap  8854  divcanap4  8857  divsubdirap  8866  divcanap5  8872  divdiv32ap  8878  divdivap2  8882  div2subap  8995  letrp1  9006  ltmulgt12  9023  lediv1  9027  ltdiv2  9045  lediv2  9049  lbinfle  9108  difgtsumgt  9527  xrletr  10016  xrre2  10029  xaddass  10077  ixxdisj  10111  ubioc1  10137  lbico1  10138  elioo5  10141  iccsupr  10174  lbicc2  10192  ubicc2  10193  iccneg  10197  icoshft  10198  icodisj  10200  iccf1o  10212  iccen  10214  zltaddlt1le  10215  fztri3or  10247  fzdcel  10248  fzen  10251  uzsubsubfz  10255  fzrevral2  10314  fzshftral  10316  fz0fzdiffz0  10338  difelfznle  10343  fzo1fzo0n0  10395  fzonmapblen  10399  fzosubel2  10413  ubmelfzo  10418  elfzodifsumelfzo  10419  ssfzo12bi  10443  ubmelm1fzo  10444  subfzo0  10460  ceiqle  10547  modqid2  10585  zmodidfzoimp  10588  addmodidr  10607  modfzo0difsn  10629  addmodlteq  10632  frec2uzf1od  10640  exprecap  10814  expdivap  10824  expubnd  10830  sqdivap  10837  mulbinom2  10890  bernneq2  10895  mulsubdivbinom2ap  10945  bcval3  10985  bccmpl  10988  omgadd  11036  ccatval1  11145  ccatval2  11146  ccatass  11156  lswccatn0lsw  11159  ccatws1lenp1bg  11183  pfxfv  11231  pfxnd  11236  pfxtrcfv  11240  pfxsuffeqwrdeq  11245  swrdswrd  11252  pfxpfx  11255  ccatopth2  11264  pfxccatin12lem4  11273  pfxccatin12lem1  11275  pfxccatin12lem2  11278  pfxccatin12lem3  11279  pfxccatin12  11280  pfxccat3  11281  swrdccat  11282  pfxccatpfx1  11283  pfxccatpfx2  11284  s3fv0g  11338  s3fv1g  11339  shftval2  11352  mulreap  11390  elicc4abs  11620  abssubge0  11628  abssuble0  11629  maxleast  11739  maxltsup  11744  xrmaxltsup  11784  xrmineqinf  11795  xrltmininf  11796  xrlemininf  11797  fsumdifsnconst  11981  prodfap0  12071  prodfrecap  12072  fprodabs  12142  sin01gt0  12288  cos01gt0  12289  sin02gt0  12290  dvdscmul  12344  summodnegmod  12348  modmulconst  12349  dvdsleabs  12371  dvdsleabs2  12372  addmodlteqALT  12385  dvdsexp  12387  mulmoddvds  12389  divalgb  12451  divgcdz  12507  gcdass  12551  mulgcdr  12554  gcddiv  12555  uzwodc  12573  lcmass  12622  coprmdvds  12629  qredeq  12633  qredeu  12634  congr  12637  divgcdcoprm0  12638  divgcdcoprmex  12639  cncongr1  12640  cncongr2  12641  isprm3  12655  dvdsnprmd  12662  euclemma  12683  prmdvdsexpb  12686  prmexpb  12688  rpexp  12690  znege1  12715  modprminv  12787  modprminveq  12788  vfermltl  12789  modprm0  12792  modprmn0modprm0  12794  coprimeprodsq  12795  coprimeprodsq2  12796  pythagtriplem1  12803  pythagtriplem3  12805  pythagtriplem6  12808  pythagtriplem12  12813  pythagtriplem13  12814  pythagtriplem14  12815  pythagtriplem16  12817  pythagtriplem19  12820  pythagtrip  12821  pcmul  12839  pcdiv  12840  pcqcl  12844  pcgcd1  12866  pcgcd  12867  dvdsprmpweq  12873  difsqpwdvds  12876  pcfaclem  12887  unbendc  13040  strle3g  13156  ercpbl  13379  grpinvid1  13600  grpinvid2  13601  grpasscan1  13611  grpasscan2  13612  grpidrcan  13613  grpidlcan  13614  grpinvadd  13626  grpsubadd  13636  grppncan  13639  pwsinvg  13660  qussub  13789  subcmnd  13885  mulgass2  14036  dvrcan1  14119  dvrcan3  14120  rmodislmodlem  14329  rmodislmod  14330  islssm  14336  lsselg  14340  lspss  14378  lspssp  14382  lsslsp  14408  islidlm  14458  lidlnegcl  14464  lidlsubcl  14466  zndvds  14628  basgen  14769  clsss  14807  ntrin  14813  ntrcls0  14820  neiint  14834  neiss  14839  neipsm  14843  opnssneib  14845  innei  14852  restco  14863  iscnp  14888  cnconst2  14922  txcn  14964  psmetsym  15018  psmetlecl  15023  distspace  15024  xmetlecl  15056  xmetsym  15057  xblcntrps  15102  xblcntr  15103  blssec  15127  blpnfctr  15128  txmetcn  15208  cnmet  15219  dvid  15384  dvidre  15386  dvply1  15454  ptolemy  15513  sinq12gt0  15519  sincosq1eq  15528  rpcxpsub  15597  relogbexpap  15647  logbleb  15650  logblt  15651  rplogbcxp  15652  lgsval4  15714  lgsmod  15720  lgsne0  15732  lgsmulsqcoprm  15740  2lgsoddprmlem1  15799  structiedg0val  15856  lpvtx  15894  upgredg2vtx  15961  upgredgpr  15962  ushgredgedg  16039  ushgredgedgloop  16041  wlkeq  16095  clwwlkccatlem  16137  clwwlkccat  16138