Theorem 3adant3 984

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

Syntax hints:   → wi 4   ∧ wa 103   ∧ w3a 945

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

This theorem depends on definitions:  df-bi 116  df-3an 947

This theorem is referenced by:  stoic4a  1391  stoic4b  1392  vtoclgft  2707  eqeu  2823  tpssi  3652  issod  4201  sotricim  4205  soinxp  4569  funopg  5115  fnco  5189  resasplitss  5260  resdif  5345  fnimapr  5435  ftpg  5558  fsnunfv  5575  fvpr1g  5580  fvpr2g  5581  f1ocnvfvb  5635  f1oiso2  5682  moriotass  5712  f1ofveu  5716  acexmid  5727  ovig  5846  ov6g  5862  ovg  5863  ot1stg  6004  ot2ndg  6005  poxp  6083  brtposg  6105  smores3  6144  smoiso  6153  rdgivallem  6232  frecsuclem  6257  nnaord  6359  nnaword  6361  nnawordex  6378  ecopovtrn  6480  ecopovtrng  6483  xpdom3m  6681  mapxpen  6695  sbthlemi4  6800  djuenun  7016  ltsopi  7076  addcanpig  7090  distrnqg  7143  ltsonq  7154  ltanqg  7156  ltmnqg  7157  nnanq0  7214  distrnq0  7215  distnq0r  7219  prarloclem  7257  genpassl  7280  genpassu  7281  distrlem1prl  7338  distrlem1pru  7339  distrlem5prl  7342  distrlem5pru  7343  1idprl  7346  1idpru  7347  ltpopr  7351  ltsopr  7352  ltexprlemm  7356  ltexprlemfl  7365  ltexprlemfu  7367  addcanprlemu  7371  recexprlem1ssl  7389  recexprlem1ssu  7390  aptipr  7397  lttrsr  7505  ltsosr  7507  ltasrg  7513  recexgt0sr  7516  mulextsr1  7523  axmulass  7608  ltxrlt  7754  axltwlin  7756  axlttrn  7757  axltadd  7758  letr  7770  mul12  7814  add12  7843  subadd  7888  addsub  7896  npncan  7906  nppcan  7907  nnpcan  7908  nppcan3  7909  pnpcan  7924  pnncan  7926  ppncan  7927  subdi  8066  ltaddsub2  8118  leaddsub2  8120  ltaddsublt  8251  apreap  8267  lemul1  8273  reapmul1lem  8274  reapadd1  8276  reapcotr  8278  receuap  8343  divassap  8363  div23ap  8364  divmulassap  8368  divmulasscomap  8369  divcanap4  8372  divsubdirap  8381  divcanap5  8387  divdiv32ap  8393  divdivap2  8397  div2subap  8509  letrp1  8516  ltmulgt12  8533  lediv1  8537  ltdiv2  8555  lediv2  8559  lbinfle  8618  xrletr  9484  xrre2  9497  xaddass  9545  ixxdisj  9579  ubioc1  9605  lbico1  9606  elioo5  9609  iccsupr  9642  lbicc2  9660  ubicc2  9661  iccneg  9665  icoshft  9666  icodisj  9668  iccf1o  9680  zltaddlt1le  9682  fztri3or  9712  fzdcel  9713  fzen  9716  uzsubsubfz  9720  fzrevral2  9779  fzshftral  9781  fz0fzdiffz0  9800  difelfznle  9805  fzo1fzo0n0  9853  fzonmapblen  9857  fzosubel2  9865  ubmelfzo  9870  elfzodifsumelfzo  9871  ssfzo12bi  9895  ubmelm1fzo  9896  subfzo0  9912  ceiqle  9979  modqid2  10017  zmodidfzoimp  10020  addmodidr  10039  modfzo0difsn  10061  addmodlteq  10064  frec2uzf1od  10072  exprecap  10227  expdivap  10237  expubnd  10243  sqdivap  10250  mulbinom2  10301  bernneq2  10306  bcval3  10390  bccmpl  10393  omgadd  10441  shftval2  10491  mulreap  10529  elicc4abs  10758  abssubge0  10766  abssuble0  10767  maxleast  10877  maxltsup  10882  xrmaxltsup  10919  xrmineqinf  10930  xrltmininf  10931  xrlemininf  10932  fsumdifsnconst  11116  sin01gt0  11319  cos01gt0  11320  sin02gt0  11321  dvdscmul  11368  summodnegmod  11372  modmulconst  11373  dvdsleabs  11391  dvdsleabs2  11392  addmodlteqALT  11405  dvdsexp  11407  mulmoddvds  11409  divalgb  11470  divgcdz  11508  gcdass  11549  mulgcdr  11552  gcddiv  11553  lcmass  11612  coprmdvds  11619  qredeq  11623  qredeu  11624  congr  11627  divgcdcoprm0  11628  divgcdcoprmex  11629  cncongr1  11630  cncongr2  11631  isprm3  11645  dvdsnprmd  11652  euclemma  11670  prmdvdsexpb  11673  prmexpb  11675  rpexp  11677  znege1  11701  strle3g  11894  basgen  12092  clsss  12130  ntrin  12136  ntrcls0  12143  neiint  12157  neiss  12162  neipsm  12166  opnssneib  12168  innei  12175  restco  12186  iscnp  12210  cnconst2  12244  txcn  12286  psmetsym  12318  psmetlecl  12323  distspace  12324  xmetlecl  12356  xmetsym  12357  xblcntrps  12402  xblcntr  12403  blssec  12427  blpnfctr  12428  txmetcn  12508  cnmet  12519  dvid  12617