Theorem 3adant3 1006

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

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

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

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

This theorem is referenced by:  stoic4a  1419  stoic4b  1420  vtoclgft  2771  eqeu  2891  tpssi  3733  issod  4291  sotricim  4295  soinxp  4668  funopg  5216  fnco  5290  resasplitss  5361  resdif  5448  fnimapr  5540  ftpg  5663  fsnunfv  5680  fvpr1g  5685  fvpr2g  5686  f1ocnvfvb  5742  f1oiso2  5789  moriotass  5820  f1ofveu  5824  acexmid  5835  ovig  5954  ov6g  5970  ovg  5971  ot1stg  6112  ot2ndg  6113  poxp  6191  brtposg  6213  smores3  6252  smoiso  6261  rdgivallem  6340  frecsuclem  6365  nnaord  6468  nnaword  6470  nnawordex  6487  ecopovtrn  6589  ecopovtrng  6592  xpdom3m  6791  mapxpen  6805  sbthlemi4  6916  djuenun  7159  ltsopi  7252  addcanpig  7266  distrnqg  7319  ltsonq  7330  ltanqg  7332  ltmnqg  7333  nnanq0  7390  distrnq0  7391  distnq0r  7395  prarloclem  7433  genpassl  7456  genpassu  7457  distrlem1prl  7514  distrlem1pru  7515  distrlem5prl  7518  distrlem5pru  7519  1idprl  7522  1idpru  7523  ltpopr  7527  ltsopr  7528  ltexprlemm  7532  ltexprlemfl  7541  ltexprlemfu  7543  addcanprlemu  7547  recexprlem1ssl  7565  recexprlem1ssu  7566  aptipr  7573  lttrsr  7694  ltsosr  7696  ltasrg  7702  recexgt0sr  7705  mulextsr1  7713  axmulass  7805  ltxrlt  7955  axltwlin  7957  axlttrn  7958  axltadd  7959  letr  7972  mul12  8018  add12  8047  subadd  8092  addsub  8100  npncan  8110  nppcan  8111  nnpcan  8112  nppcan3  8113  pnpcan  8128  pnncan  8130  ppncan  8131  subdi  8274  ltaddsub2  8326  leaddsub2  8328  ltaddsublt  8460  apreap  8476  lemul1  8482  reapmul1lem  8483  reapadd1  8485  reapcotr  8487  receuap  8557  divassap  8577  div23ap  8578  divmulassap  8582  divmulasscomap  8583  divcanap4  8586  divsubdirap  8595  divcanap5  8601  divdiv32ap  8607  divdivap2  8611  div2subap  8724  letrp1  8734  ltmulgt12  8751  lediv1  8755  ltdiv2  8773  lediv2  8777  lbinfle  8836  difgtsumgt  9251  xrletr  9735  xrre2  9748  xaddass  9796  ixxdisj  9830  ubioc1  9856  lbico1  9857  elioo5  9860  iccsupr  9893  lbicc2  9911  ubicc2  9912  iccneg  9916  icoshft  9917  icodisj  9919  iccf1o  9931  iccen  9933  zltaddlt1le  9934  fztri3or  9964  fzdcel  9965  fzen  9968  uzsubsubfz  9972  fzrevral2  10031  fzshftral  10033  fz0fzdiffz0  10055  difelfznle  10060  fzo1fzo0n0  10108  fzonmapblen  10112  fzosubel2  10120  ubmelfzo  10125  elfzodifsumelfzo  10126  ssfzo12bi  10150  ubmelm1fzo  10151  subfzo0  10167  ceiqle  10238  modqid2  10276  zmodidfzoimp  10279  addmodidr  10298  modfzo0difsn  10320  addmodlteq  10323  frec2uzf1od  10331  exprecap  10486  expdivap  10496  expubnd  10502  sqdivap  10509  mulbinom2  10560  bernneq2  10565  bcval3  10653  bccmpl  10656  omgadd  10704  shftval2  10754  mulreap  10792  elicc4abs  11022  abssubge0  11030  abssuble0  11031  maxleast  11141  maxltsup  11146  xrmaxltsup  11185  xrmineqinf  11196  xrltmininf  11197  xrlemininf  11198  fsumdifsnconst  11382  prodfap0  11472  prodfrecap  11473  fprodabs  11543  sin01gt0  11688  cos01gt0  11689  sin02gt0  11690  dvdscmul  11744  summodnegmod  11748  modmulconst  11749  dvdsleabs  11768  dvdsleabs2  11769  addmodlteqALT  11782  dvdsexp  11784  mulmoddvds  11786  divalgb  11847  divgcdz  11889  gcdass  11933  mulgcdr  11936  gcddiv  11937  lcmass  11996  coprmdvds  12003  qredeq  12007  qredeu  12008  congr  12011  divgcdcoprm0  12012  divgcdcoprmex  12013  cncongr1  12014  cncongr2  12015  isprm3  12029  dvdsnprmd  12036  euclemma  12055  prmdvdsexpb  12058  prmexpb  12060  rpexp  12062  znege1  12087  modprminv  12158  modprminveq  12159  vfermltl  12160  modprm0  12163  modprmn0modprm0  12165  coprimeprodsq  12166  coprimeprodsq2  12167  pythagtriplem1  12174  pythagtriplem3  12176  pythagtriplem6  12179  pythagtriplem12  12184  pythagtriplem13  12185  pythagtriplem14  12186  pythagtriplem16  12188  pythagtriplem19  12191  pythagtrip  12192  pcmul  12210  pcdiv  12211  pcqcl  12215  pcgcd1  12236  pcgcd  12237  dvdsprmpweq  12243  difsqpwdvds  12246  pcfaclem  12256  unbendc  12326  strle3g  12423  basgen  12621  clsss  12659  ntrin  12665  ntrcls0  12672  neiint  12686  neiss  12691  neipsm  12695  opnssneib  12697  innei  12704  restco  12715  iscnp  12740  cnconst2  12774  txcn  12816  psmetsym  12870  psmetlecl  12875  distspace  12876  xmetlecl  12908  xmetsym  12909  xblcntrps  12954  xblcntr  12955  blssec  12979  blpnfctr  12980  txmetcn  13060  cnmet  13071  dvid  13203  ptolemy  13286  sinq12gt0  13292  sincosq1eq  13301  rpcxpsub  13370  relogbexpap  13417  logbleb  13420  logblt  13421  rplogbcxp  13422