Theorem 3adant3 959

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

Syntax hints:   → wi 4   ∧ wa 102   ∧ w3a 920

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104

This theorem depends on definitions:  df-bi 115  df-3an 922

This theorem is referenced by:  stoic4a  1362  stoic4b  1363  vtoclgft  2660  eqeu  2773  tpssi  3577  issod  4110  sotricim  4114  soinxp  4466  funopg  5001  fnco  5075  resasplitss  5138  resdif  5223  fnimapr  5309  ftpg  5423  fsnunfv  5439  fvpr1g  5443  fvpr2g  5444  f1ocnvfvb  5499  f1oiso2  5545  moriotass  5575  f1ofveu  5579  acexmid  5590  ovig  5701  ov6g  5717  ovg  5718  ot1stg  5858  ot2ndg  5859  poxp  5932  brtposg  5951  smores3  5990  smoiso  5999  rdgivallem  6078  frecsuclem  6103  nnaord  6198  nnaword  6200  nnawordex  6217  ecopovtrn  6319  ecopovtrng  6322  xpdom3m  6480  mapxpen  6494  ltsopi  6782  addcanpig  6796  distrnqg  6849  ltsonq  6860  ltanqg  6862  ltmnqg  6863  nnanq0  6920  distrnq0  6921  distnq0r  6925  prarloclem  6963  genpassl  6986  genpassu  6987  distrlem1prl  7044  distrlem1pru  7045  distrlem5prl  7048  distrlem5pru  7049  1idprl  7052  1idpru  7053  ltpopr  7057  ltsopr  7058  ltexprlemm  7062  ltexprlemfl  7071  ltexprlemfu  7073  addcanprlemu  7077  recexprlem1ssl  7095  recexprlem1ssu  7096  aptipr  7103  lttrsr  7211  ltsosr  7213  ltasrg  7219  recexgt0sr  7222  mulextsr1  7229  axmulass  7311  ltxrlt  7455  axltwlin  7457  axlttrn  7458  axltadd  7459  letr  7471  mul12  7514  add12  7543  subadd  7588  addsub  7596  npncan  7606  nppcan  7607  nnpcan  7608  nppcan3  7609  pnpcan  7624  pnncan  7626  ppncan  7627  subdi  7766  ltaddsub2  7818  leaddsub2  7820  ltaddsublt  7948  apreap  7964  lemul1  7970  reapmul1lem  7971  reapadd1  7973  reapcotr  7975  receuap  8036  divassap  8055  div23ap  8056  divmulassap  8060  divmulasscomap  8061  divcanap4  8064  divsubdirap  8073  divcanap5  8079  divdiv32ap  8085  divdivap2  8089  letrp1  8203  ltmulgt12  8220  lediv1  8224  ltdiv2  8242  lediv2  8246  lbinfle  8305  xrletr  9168  xrre2  9178  ixxdisj  9216  ubioc1  9242  lbico1  9243  elioo5  9246  iccsupr  9279  lbicc2  9296  ubicc2  9297  iccneg  9301  icoshft  9302  icodisj  9304  iccf1o  9316  zltaddlt1le  9318  fztri3or  9348  fzdcel  9349  fzen  9352  uzsubsubfz  9356  fzrevral2  9413  fzshftral  9415  fz0fzdiffz0  9432  difelfznle  9437  fzo1fzo0n0  9483  fzonmapblen  9487  fzosubel2  9495  ubmelfzo  9500  elfzodifsumelfzo  9501  ssfzo12bi  9525  ubmelm1fzo  9526  subfzo0  9542  ceiqle  9609  modqid2  9647  zmodidfzoimp  9650  addmodidr  9669  modfzo0difsn  9691  addmodlteq  9694  frec2uzf1od  9702  exprecap  9833  expdivap  9843  expubnd  9849  sqdivap  9856  mulbinom2  9905  bernneq2  9910  bcval3  9994  bccmpl  9997  omgadd  10045  shftval2  10088  mulreap  10125  elicc4abs  10354  abssubge0  10362  abssuble0  10363  maxleast  10473  maxltsup  10478  dvdscmul  10603  summodnegmod  10607  modmulconst  10608  dvdsleabs  10626  dvdsleabs2  10627  addmodlteqALT  10640  dvdsexp  10642  mulmoddvds  10644  divalgb  10705  divgcdz  10743  gcdass  10784  mulgcdr  10787  gcddiv  10788  lcmass  10847  coprmdvds  10854  qredeq  10858  qredeu  10859  congr  10862  divgcdcoprm0  10863  divgcdcoprmex  10864  cncongr1  10865  cncongr2  10866  isprm3  10880  dvdsnprmd  10887  euclemma  10905  prmdvdsexpb  10908  prmexpb  10910  rpexp  10912  znege1  10936