Theorem 3adant3 1017

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

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

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 980

This theorem is referenced by:  stoic4a  1432  stoic4b  1433  vtoclgft  2789  eqeu  2909  tpssi  3761  issod  4321  sotricim  4325  soinxp  4698  funopg  5252  fnco  5326  resasplitss  5397  resdif  5485  fnimapr  5578  ftpg  5702  fsnunfv  5719  fvpr1g  5724  fvpr2g  5725  f1ocnvfvb  5783  f1oiso2  5830  moriotass  5861  f1ofveu  5865  acexmid  5876  ovig  5998  ov6g  6014  ovg  6015  ot1stg  6155  ot2ndg  6156  poxp  6235  brtposg  6257  smores3  6296  smoiso  6305  rdgivallem  6384  frecsuclem  6409  nnaord  6512  nnaword  6514  nnawordex  6532  ecopovtrn  6634  ecopovtrng  6637  xpdom3m  6836  mapxpen  6850  sbthlemi4  6961  djuenun  7213  netap  7255  2omotaplemap  7258  ltsopi  7321  addcanpig  7335  distrnqg  7388  ltsonq  7399  ltanqg  7401  ltmnqg  7402  nnanq0  7459  distrnq0  7460  distnq0r  7464  prarloclem  7502  genpassl  7525  genpassu  7526  distrlem1prl  7583  distrlem1pru  7584  distrlem5prl  7587  distrlem5pru  7588  1idprl  7591  1idpru  7592  ltpopr  7596  ltsopr  7597  ltexprlemm  7601  ltexprlemfl  7610  ltexprlemfu  7612  addcanprlemu  7616  recexprlem1ssl  7634  recexprlem1ssu  7635  aptipr  7642  lttrsr  7763  ltsosr  7765  ltasrg  7771  recexgt0sr  7774  mulextsr1  7782  axmulass  7874  ltxrlt  8025  axltwlin  8027  axlttrn  8028  axltadd  8029  letr  8042  mul12  8088  add12  8117  subadd  8162  addsub  8170  npncan  8180  nppcan  8181  nnpcan  8182  nppcan3  8183  pnpcan  8198  pnncan  8200  ppncan  8201  subdi  8344  ltaddsub2  8396  leaddsub2  8398  ltaddsublt  8530  apreap  8546  lemul1  8552  reapmul1lem  8553  reapadd1  8555  reapcotr  8557  receuap  8628  divassap  8649  div23ap  8650  divmulassap  8654  divmulasscomap  8655  divcanap4  8658  divsubdirap  8667  divcanap5  8673  divdiv32ap  8679  divdivap2  8683  div2subap  8796  letrp1  8807  ltmulgt12  8824  lediv1  8828  ltdiv2  8846  lediv2  8850  lbinfle  8909  difgtsumgt  9324  xrletr  9810  xrre2  9823  xaddass  9871  ixxdisj  9905  ubioc1  9931  lbico1  9932  elioo5  9935  iccsupr  9968  lbicc2  9986  ubicc2  9987  iccneg  9991  icoshft  9992  icodisj  9994  iccf1o  10006  iccen  10008  zltaddlt1le  10009  fztri3or  10041  fzdcel  10042  fzen  10045  uzsubsubfz  10049  fzrevral2  10108  fzshftral  10110  fz0fzdiffz0  10132  difelfznle  10137  fzo1fzo0n0  10185  fzonmapblen  10189  fzosubel2  10197  ubmelfzo  10202  elfzodifsumelfzo  10203  ssfzo12bi  10227  ubmelm1fzo  10228  subfzo0  10244  ceiqle  10315  modqid2  10353  zmodidfzoimp  10356  addmodidr  10375  modfzo0difsn  10397  addmodlteq  10400  frec2uzf1od  10408  exprecap  10563  expdivap  10573  expubnd  10579  sqdivap  10586  mulbinom2  10639  bernneq2  10644  mulsubdivbinom2ap  10693  bcval3  10733  bccmpl  10736  omgadd  10784  shftval2  10837  mulreap  10875  elicc4abs  11105  abssubge0  11113  abssuble0  11114  maxleast  11224  maxltsup  11229  xrmaxltsup  11268  xrmineqinf  11279  xrltmininf  11280  xrlemininf  11281  fsumdifsnconst  11465  prodfap0  11555  prodfrecap  11556  fprodabs  11626  sin01gt0  11771  cos01gt0  11772  sin02gt0  11773  dvdscmul  11827  summodnegmod  11831  modmulconst  11832  dvdsleabs  11853  dvdsleabs2  11854  addmodlteqALT  11867  dvdsexp  11869  mulmoddvds  11871  divalgb  11932  divgcdz  11974  gcdass  12018  mulgcdr  12021  gcddiv  12022  uzwodc  12040  lcmass  12087  coprmdvds  12094  qredeq  12098  qredeu  12099  congr  12102  divgcdcoprm0  12103  divgcdcoprmex  12104  cncongr1  12105  cncongr2  12106  isprm3  12120  dvdsnprmd  12127  euclemma  12148  prmdvdsexpb  12151  prmexpb  12153  rpexp  12155  znege1  12180  modprminv  12251  modprminveq  12252  vfermltl  12253  modprm0  12256  modprmn0modprm0  12258  coprimeprodsq  12259  coprimeprodsq2  12260  pythagtriplem1  12267  pythagtriplem3  12269  pythagtriplem6  12272  pythagtriplem12  12277  pythagtriplem13  12278  pythagtriplem14  12279  pythagtriplem16  12281  pythagtriplem19  12284  pythagtrip  12285  pcmul  12303  pcdiv  12304  pcqcl  12308  pcgcd1  12329  pcgcd  12330  dvdsprmpweq  12336  difsqpwdvds  12339  pcfaclem  12349  unbendc  12457  strle3g  12569  ercpbl  12755  grpinvid1  12929  grpinvid2  12930  grpasscan1  12938  grpasscan2  12939  grpidrcan  12940  grpidlcan  12941  grpinvadd  12953  grpsubadd  12963  grppncan  12966  subcmnd  13134  mulgass2  13240  dvrcan1  13314  dvrcan3  13315  rmodislmodlem  13445  rmodislmod  13446  lsselg  13453  basgen  13619  clsss  13657  ntrin  13663  ntrcls0  13670  neiint  13684  neiss  13689  neipsm  13693  opnssneib  13695  innei  13702  restco  13713  iscnp  13738  cnconst2  13772  txcn  13814  psmetsym  13868  psmetlecl  13873  distspace  13874  xmetlecl  13906  xmetsym  13907  xblcntrps  13952  xblcntr  13953  blssec  13977  blpnfctr  13978  txmetcn  14058  cnmet  14069  dvid  14201  ptolemy  14284  sinq12gt0  14290  sincosq1eq  14299  rpcxpsub  14368  relogbexpap  14415  logbleb  14418  logblt  14419  rplogbcxp  14420  lgsval4  14460  lgsmod  14466  lgsne0  14478  lgsmulsqcoprm  14486  2lgsoddprmlem1  14492