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 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜃) → 𝜒)

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

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 1011

This theorem is referenced by:  stoic4a  1481  stoic4b  1482  vtoclgft  2873  eqeu  2996  ssprsseq  3872  tpssi  3879  issod  4459  sotricim  4463  soinxp  4840  funopg  5406  fnco  5486  resasplitss  5564  resdif  5656  fnimapr  5757  ftpg  5890  fsnunfv  5907  fvpr1g  5912  fvpr2g  5913  f1ocnvfvb  5976  f1oiso2  6023  moriotass  6059  f1ofveu  6063  acexmid  6074  ovig  6200  ov6g  6217  ovg  6218  ot1stg  6376  ot2ndg  6377  poxp  6458  suppvalfn  6471  suppsnopdc  6480  suppfnss  6487  funsssuppss  6488  brtposg  6515  smores3  6554  smoiso  6563  rdgivallem  6642  frecsuclem  6667  nnaord  6772  nnaword  6774  nnawordex  6792  ecopovtrn  6896  ecopovtrng  6899  xpdom3m  7122  mapxpen  7138  sbthlemi4  7267  djuenun  7558  netap  7610  2omotaplemap  7613  ltsopi  7677  addcanpig  7691  distrnqg  7744  ltsonq  7755  ltanqg  7757  ltmnqg  7758  nnanq0  7815  distrnq0  7816  distnq0r  7820  prarloclem  7858  genpassl  7881  genpassu  7882  distrlem1prl  7939  distrlem1pru  7940  distrlem5prl  7943  distrlem5pru  7944  1idprl  7947  1idpru  7948  ltpopr  7952  ltsopr  7953  ltexprlemm  7957  ltexprlemfl  7966  ltexprlemfu  7968  addcanprlemu  7972  recexprlem1ssl  7990  recexprlem1ssu  7991  aptipr  7998  lttrsr  8119  ltsosr  8121  ltasrg  8127  recexgt0sr  8130  mulextsr1  8138  axmulass  8230  ltxrlt  8381  axltwlin  8383  axlttrn  8384  axltadd  8385  letr  8398  mul12  8445  add12  8474  subadd  8519  addsub  8527  npncan  8537  nppcan  8538  nnpcan  8539  nppcan3  8540  pnpcan  8555  pnncan  8557  ppncan  8558  subdi  8702  ltaddsub2  8755  leaddsub2  8757  ltaddsublt  8889  apreap  8905  lemul1  8911  reapmul1lem  8912  reapadd1  8914  reapcotr  8916  receuap  8989  divassap  9010  div23ap  9011  divmulassap  9015  divmulasscomap  9016  divcanap4  9019  divsubdirap  9028  divcanap5  9034  divdiv32ap  9040  divdivap2  9044  div2subap  9157  letrp1  9168  ltmulgt12  9185  lediv1  9189  ltdiv2  9207  lediv2  9211  lbinfle  9270  difgtsumgt  9693  xrletr  10189  xrre2  10202  xaddass  10250  ixxdisj  10284  ubioc1  10310  lbico1  10311  elioo5  10314  iccsupr  10347  lbicc2  10365  ubicc2  10366  iccneg  10370  icoshft  10371  icodisj  10373  lincmble  10385  iccf1o  10386  iccen  10388  zltaddlt1le  10389  fztri3or  10422  fzdcel  10423  fzen  10426  uzsubsubfz  10430  fzrevral2  10491  fzshftral  10493  fz0fzdiffz0  10515  difelfznle  10520  fzo1fzo0n0  10573  fzonmapblen  10577  fzosubel2  10591  ubmelfzo  10596  elfzodifsumelfzo  10597  ssfzo12bi  10621  ubmelm1fzo  10622  subfzo0  10639  ceiqle  10728  modqid2  10766  zmodidfzoimp  10769  addmodidr  10788  modfzo0difsn  10810  addmodlteq  10813  frec2uzf1od  10821  exprecap  10995  expdivap  11005  expubnd  11011  sqdivap  11018  mulbinom2  11071  bernneq2  11077  mulsubdivbinom2ap  11127  bcval3  11167  bccmpl  11170  omgadd  11220  ccatval1  11343  ccatval2  11344  ccatass  11354  lswccatn0lsw  11357  ccatws1lenp1bg  11381  ccatw2s1leng  11384  pfxfv  11434  pfxnd  11439  pfxtrcfv  11443  pfxsuffeqwrdeq  11448  swrdswrd  11455  pfxpfx  11458  ccatopth2  11467  pfxccatin12lem4  11476  pfxccatin12lem1  11478  pfxccatin12lem2  11481  pfxccatin12lem3  11482  pfxccatin12  11483  pfxccat3  11484  swrdccat  11485  pfxccatpfx1  11486  pfxccatpfx2  11487  s3fv0g  11541  s3fv1g  11542  s3fv2g  11543  shftval2  11569  mulreap  11607  elicc4abs  11838  abssubge0  11846  abssuble0  11847  maxleast  11957  maxltsup  11962  xrmaxltsup  12002  xrmineqinf  12013  xrltmininf  12014  xrlemininf  12015  fsumdifsnconst  12200  prodfap0  12290  prodfrecap  12291  fprodabs  12361  sin01gt0  12507  cos01gt0  12508  sin02gt0  12509  dvdscmul  12563  summodnegmod  12567  modmulconst  12568  dvdsleabs  12590  dvdsleabs2  12591  addmodlteqALT  12604  dvdsexp  12606  mulmoddvds  12608  divalgb  12670  divgcdz  12726  gcdass  12770  mulgcdr  12773  gcddiv  12774  uzwodc  12792  lcmass  12841  coprmdvds  12848  qredeq  12852  qredeu  12853  congr  12856  divgcdcoprm0  12857  divgcdcoprmex  12858  cncongr1  12859  cncongr2  12860  isprm3  12874  dvdsnprmd  12881  euclemma  12902  prmdvdsexpb  12905  prmexpb  12907  rpexp  12909  znege1  12934  modprminv  13006  modprminveq  13007  vfermltl  13008  modprm0  13011  modprmn0modprm0  13013  coprimeprodsq  13014  coprimeprodsq2  13015  pythagtriplem1  13022  pythagtriplem3  13024  pythagtriplem6  13027  pythagtriplem12  13032  pythagtriplem13  13033  pythagtriplem14  13034  pythagtriplem16  13036  pythagtriplem19  13039  pythagtrip  13040  pcmul  13058  pcdiv  13059  pcqcl  13063  pcgcd1  13085  pcgcd  13086  dvdsprmpweq  13092  difsqpwdvds  13095  pcfaclem  13106  ballotfilemsgt1  13232  ballotfilemrv1  13242  ballotfilemrv2  13243  ballotfilemfrcn0  13251  unbendc  13323  strle3g  13439  ercpbl  13629  grpinvid1  13834  grpinvid2  13835  grpasscan1  13845  grpasscan2  13846  grpidrcan  13847  grpidlcan  13848  grpinvadd  13860  grpsubadd  13870  grppncan  13873  qussub  14017  subcmnd  14114  pwsinvg  14192  rng1zrlem  14233  mulgass2  14336  dvrcan1  14420  dvrcan3  14421  rmodislmodlem  14659  rmodislmod  14660  islssm  14666  lsselg  14670  lspss  14708  lspssp  14712  lsslsp  14738  islidlm  14788  lidlnegcl  14794  lidlsubcl  14796  zndvds  14956  basgen  15104  clsss  15142  ntrin  15148  ntrcls0  15155  neiint  15169  neiss  15174  neipsm  15178  opnssneib  15180  innei  15187  restco  15198  iscnp  15223  cnconst2  15257  txcn  15299  psmetsym  15353  psmetlecl  15358  distspace  15359  xmetlecl  15391  xmetsym  15392  xblcntrps  15437  xblcntr  15438  blssec  15462  blpnfctr  15463  txmetcn  15543  cnmet  15554  dvid  15719  dvidre  15721  dvply1  15789  ptolemy  15848  sinq12gt0  15854  sincosq1eq  15863  rpcxpsub  15933  relogbexpap  15983  logbleb  15986  logblt  15987  rplogbcxp  15988  lgsval4  16053  lgsmod  16059  lgsne0  16071  lgsmulsqcoprm  16079  2lgsoddprmlem1  16138  structiedg0val  16195  lpvtx  16234  upgredg2vtx  16303  upgredgpr  16304  ushgredgedg  16381  ushgredgedgloop  16383  usgr2v1e2w  16401  wlkeq  16509  clwwlkccatlem  16555  clwwlkccat  16556  clwwlkext2edg  16577  clwwlknccat  16578  s2elclwwlknon2  16591  clwwlknonex2lem2  16593  repiecele0  16980  repiecege0  16981