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  4466  sotricim  4470  soinxp  4847  funopg  5414  fnco  5494  resasplitss  5572  resdif  5664  fnimapr  5766  ftpg  5902  fsnunfv  5919  fvpr1g  5924  fvpr2g  5925  f1ocnvfvb  5989  f1oiso2  6036  moriotass  6072  f1ofveu  6076  acexmid  6087  ovig  6213  ov6g  6230  ovg  6231  ot1stg  6390  ot2ndg  6391  poxp  6472  suppvalfn  6485  suppsnopdc  6494  suppfnss  6501  funsssuppss  6502  brtposg  6530  smores3  6569  smoiso  6578  rdgivallem  6657  frecsuclem  6682  nnaord  6787  nnaword  6789  nnawordex  6807  ecopovtrn  6911  ecopovtrng  6914  xpdom3m  7138  mapxpen  7154  sbthlemi4  7284  snopfsupp  7306  djuenun  7574  netap  7626  2omotaplemap  7629  ltsopi  7693  addcanpig  7707  distrnqg  7760  ltsonq  7771  ltanqg  7773  ltmnqg  7774  nnanq0  7831  distrnq0  7832  distnq0r  7836  prarloclem  7874  genpassl  7897  genpassu  7898  distrlem1prl  7955  distrlem1pru  7956  distrlem5prl  7959  distrlem5pru  7960  1idprl  7963  1idpru  7964  ltpopr  7968  ltsopr  7969  ltexprlemm  7973  ltexprlemfl  7982  ltexprlemfu  7984  addcanprlemu  7988  recexprlem1ssl  8006  recexprlem1ssu  8007  aptipr  8014  lttrsr  8135  ltsosr  8137  ltasrg  8143  recexgt0sr  8146  mulextsr1  8154  axmulass  8246  ltxrlt  8397  axltwlin  8399  axlttrn  8400  axltadd  8401  letr  8414  mul12  8462  add12  8491  subadd  8536  addsub  8544  npncan  8554  nppcan  8555  nnpcan  8556  nppcan3  8557  pnpcan  8572  pnncan  8574  ppncan  8575  subdi  8719  ltaddsub2  8772  leaddsub2  8774  ltaddsublt  8907  apreap  8923  lemul1  8929  reapmul1lem  8930  reapadd1  8932  reapcotr  8934  receuap  9007  divassap  9028  div23ap  9029  divmulassap  9033  divmulasscomap  9034  divcanap4  9037  divsubdirap  9046  divcanap5  9052  divdiv32ap  9058  divdivap2  9062  div2subap  9175  letrp1  9186  ltmulgt12  9203  lediv1  9207  ltdiv2  9225  lediv2  9229  lbinfle  9288  indfdc  9307  indfval  9308  difgtsumgt  9723  xrletr  10226  xrre2  10239  xaddass  10287  ixxdisj  10321  ubioc1  10347  lbico1  10348  elioo5  10351  iccsupr  10384  lbicc2  10402  ubicc2  10403  iccneg  10407  icoshft  10408  icodisj  10410  lincmble  10422  iccf1o  10423  iccen  10425  zltaddlt1le  10426  fztri3or  10459  fzdcel  10460  fzen  10463  uzsubsubfz  10468  fzrevral2  10529  fzshftral  10531  fz0fzdiffz0  10553  difelfznle  10558  fzo1fzo0n0  10611  fzonmapblen  10615  fzosubel2  10629  ubmelfzo  10634  elfzodifsumelfzo  10635  ssfzo12bi  10659  ubmelm1fzo  10660  subfzo0  10677  ceiqle  10770  modqid2  10808  zmodidfzoimp  10811  addmodidr  10830  modfzo0difsn  10852  addmodlteq  10855  frec2uzf1od  10863  exprecap  11037  expdivap  11047  expubnd  11053  sqdivap  11060  mulbinom2  11113  bernneq2  11119  mulsubdivbinom2ap  11170  bcval3  11210  bccmpl  11213  omgadd  11263  ccatval1  11386  ccatval2  11387  ccatass  11397  lswccatn0lsw  11400  ccatws1lenp1bg  11424  ccatw2s1leng  11427  pfxfv  11477  pfxnd  11482  pfxtrcfv  11486  pfxsuffeqwrdeq  11491  swrdswrd  11498  pfxpfx  11501  ccatopth2  11510  pfxccatin12lem4  11519  pfxccatin12lem1  11521  pfxccatin12lem2  11524  pfxccatin12lem3  11525  pfxccatin12  11526  pfxccat3  11527  swrdccat  11528  pfxccatpfx1  11529  pfxccatpfx2  11530  s3fv0g  11584  s3fv1g  11585  s3fv2g  11586  shftval2  11612  mulreap  11650  elicc4abs  11882  abssubge0  11890  abssuble0  11891  maxleast  12001  maxltsup  12006  xrmaxltsup  12048  xrmineqinf  12059  xrltmininf  12060  xrlemininf  12061  fsumdifsnconst  12246  prodfap0  12336  prodfrecap  12337  fprodabs  12407  sin01gt0  12553  cos01gt0  12554  sin02gt0  12555  dvdscmul  12609  summodnegmod  12613  modmulconst  12614  dvdsleabs  12636  dvdsleabs2  12637  addmodlteqALT  12650  dvdsexp  12652  mulmoddvds  12654  divalgb  12716  divgcdz  12772  gcdass  12816  mulgcdr  12819  gcddiv  12820  uzwodc  12838  lcmass  12887  coprmdvds  12894  qredeq  12898  qredeu  12899  congr  12902  divgcdcoprm0  12903  divgcdcoprmex  12904  cncongr1  12905  cncongr2  12906  isprm3  12920  dvdsnprmd  12927  euclemma  12949  prmdvdsexpb  12952  prmexpb  12954  rpexp  12956  znege1  12982  modprminv  13056  modprminveq  13057  vfermltl  13058  modprm0  13061  modprmn0modprm0  13063  coprimeprodsq  13064  coprimeprodsq2  13065  pythagtriplem1  13072  pythagtriplem3  13074  pythagtriplem6  13077  pythagtriplem12  13082  pythagtriplem13  13083  pythagtriplem14  13084  pythagtriplem16  13086  pythagtriplem19  13089  pythagtrip  13090  pcmul  13108  pcdiv  13109  pcqcl  13113  pcgcd1  13135  pcgcd  13136  dvdsprmpweq  13142  difsqpwdvds  13145  pcfaclem  13156  ballotfilemsgt1  13311  ballotfilemrv1  13321  ballotfilemrv2  13322  ballotfilemfrcn0  13330  unbendc  13402  strle3g  13520  ercpbl  13710  grpinvid1  13915  grpinvid2  13916  grpasscan1  13926  grpasscan2  13927  grpidrcan  13928  grpidlcan  13929  grpinvadd  13941  grpsubadd  13951  grppncan  13954  qussub  14098  subcmnd  14226  pwsinvg  14321  rng1zrlem  14364  mulgass2  14469  dvrcan1  14555  dvrcan3  14556  rmodislmodlem  14795  rmodislmod  14796  islssm  14802  lsselg  14806  lspss  14844  lspssp  14848  lsslsp  14874  islidlm  14924  lidlnegcl  14930  lidlsubcl  14932  zndvds  15092  assa2ass  15117  assa2ass2  15118  aspss  15127  basgen  15323  clsss  15361  ntrin  15367  ntrcls0  15374  neiint  15388  neiss  15393  neipsm  15397  opnssneib  15399  innei  15406  restco  15417  iscnp  15442  cnconst2  15476  txcn  15518  psmetsym  15572  psmetlecl  15577  distspace  15578  xmetlecl  15610  xmetsym  15611  xblcntrps  15656  xblcntr  15657  blssec  15681  blpnfctr  15682  txmetcn  15762  cnmet  15773  dvid  15938  dvidre  15940  dvply1  16008  ptolemy  16068  sinq12gt0  16074  sincosq1eq  16083  rpcxpsub  16158  relogbexpap  16211  logbleb  16214  logblt  16215  rplogbcxp  16216  lgsval4  16361  lgsmod  16367  lgsne0  16379  lgsmulsqcoprm  16387  2lgsoddprmlem1  16446  structiedg0val  16503  lpvtx  16542  upgredg2vtx  16611  upgredgpr  16612  ushgredgedg  16689  ushgredgedgloop  16691  usgr2v1e2w  16709  wlkeq  16817  clwwlkccatlem  16863  clwwlkccat  16864  clwwlkext2edg  16885  clwwlknccat  16886  s2elclwwlknon2  16899  clwwlknonex2lem2  16901  repiecele0  17298  repiecege0  17299