Theorem 3adant3 1020

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

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

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 983

This theorem is referenced by:  stoic4a  1452  stoic4b  1453  vtoclgft  2825  eqeu  2947  tpssi  3805  issod  4373  sotricim  4377  soinxp  4752  funopg  5313  fnco  5392  resasplitss  5466  resdif  5555  fnimapr  5651  ftpg  5780  fsnunfv  5797  fvpr1g  5802  fvpr2g  5803  f1ocnvfvb  5861  f1oiso2  5908  moriotass  5940  f1ofveu  5944  acexmid  5955  ovig  6079  ov6g  6096  ovg  6097  ot1stg  6250  ot2ndg  6251  poxp  6330  brtposg  6352  smores3  6391  smoiso  6400  rdgivallem  6479  frecsuclem  6504  nnaord  6607  nnaword  6609  nnawordex  6627  ecopovtrn  6731  ecopovtrng  6734  xpdom3m  6943  mapxpen  6959  sbthlemi4  7076  djuenun  7339  netap  7381  2omotaplemap  7384  ltsopi  7448  addcanpig  7462  distrnqg  7515  ltsonq  7526  ltanqg  7528  ltmnqg  7529  nnanq0  7586  distrnq0  7587  distnq0r  7591  prarloclem  7629  genpassl  7652  genpassu  7653  distrlem1prl  7710  distrlem1pru  7711  distrlem5prl  7714  distrlem5pru  7715  1idprl  7718  1idpru  7719  ltpopr  7723  ltsopr  7724  ltexprlemm  7728  ltexprlemfl  7737  ltexprlemfu  7739  addcanprlemu  7743  recexprlem1ssl  7761  recexprlem1ssu  7762  aptipr  7769  lttrsr  7890  ltsosr  7892  ltasrg  7898  recexgt0sr  7901  mulextsr1  7909  axmulass  8001  ltxrlt  8153  axltwlin  8155  axlttrn  8156  axltadd  8157  letr  8170  mul12  8216  add12  8245  subadd  8290  addsub  8298  npncan  8308  nppcan  8309  nnpcan  8310  nppcan3  8311  pnpcan  8326  pnncan  8328  ppncan  8329  subdi  8472  ltaddsub2  8525  leaddsub2  8527  ltaddsublt  8659  apreap  8675  lemul1  8681  reapmul1lem  8682  reapadd1  8684  reapcotr  8686  receuap  8757  divassap  8778  div23ap  8779  divmulassap  8783  divmulasscomap  8784  divcanap4  8787  divsubdirap  8796  divcanap5  8802  divdiv32ap  8808  divdivap2  8812  div2subap  8925  letrp1  8936  ltmulgt12  8953  lediv1  8957  ltdiv2  8975  lediv2  8979  lbinfle  9038  difgtsumgt  9457  xrletr  9945  xrre2  9958  xaddass  10006  ixxdisj  10040  ubioc1  10066  lbico1  10067  elioo5  10070  iccsupr  10103  lbicc2  10121  ubicc2  10122  iccneg  10126  icoshft  10127  icodisj  10129  iccf1o  10141  iccen  10143  zltaddlt1le  10144  fztri3or  10176  fzdcel  10177  fzen  10180  uzsubsubfz  10184  fzrevral2  10243  fzshftral  10245  fz0fzdiffz0  10267  difelfznle  10272  fzo1fzo0n0  10324  fzonmapblen  10328  fzosubel2  10341  ubmelfzo  10346  elfzodifsumelfzo  10347  ssfzo12bi  10371  ubmelm1fzo  10372  subfzo0  10388  ceiqle  10475  modqid2  10513  zmodidfzoimp  10516  addmodidr  10535  modfzo0difsn  10557  addmodlteq  10560  frec2uzf1od  10568  exprecap  10742  expdivap  10752  expubnd  10758  sqdivap  10765  mulbinom2  10818  bernneq2  10823  mulsubdivbinom2ap  10873  bcval3  10913  bccmpl  10916  omgadd  10964  ccatval1  11071  ccatval2  11072  ccatass  11082  lswccatn0lsw  11085  ccatws1lenp1bg  11107  pfxfv  11155  pfxnd  11160  pfxtrcfv  11164  pfxsuffeqwrdeq  11169  swrdswrd  11176  pfxpfx  11179  ccatopth2  11188  shftval2  11207  mulreap  11245  elicc4abs  11475  abssubge0  11483  abssuble0  11484  maxleast  11594  maxltsup  11599  xrmaxltsup  11639  xrmineqinf  11650  xrltmininf  11651  xrlemininf  11652  fsumdifsnconst  11836  prodfap0  11926  prodfrecap  11927  fprodabs  11997  sin01gt0  12143  cos01gt0  12144  sin02gt0  12145  dvdscmul  12199  summodnegmod  12203  modmulconst  12204  dvdsleabs  12226  dvdsleabs2  12227  addmodlteqALT  12240  dvdsexp  12242  mulmoddvds  12244  divalgb  12306  divgcdz  12362  gcdass  12406  mulgcdr  12409  gcddiv  12410  uzwodc  12428  lcmass  12477  coprmdvds  12484  qredeq  12488  qredeu  12489  congr  12492  divgcdcoprm0  12493  divgcdcoprmex  12494  cncongr1  12495  cncongr2  12496  isprm3  12510  dvdsnprmd  12517  euclemma  12538  prmdvdsexpb  12541  prmexpb  12543  rpexp  12545  znege1  12570  modprminv  12642  modprminveq  12643  vfermltl  12644  modprm0  12647  modprmn0modprm0  12649  coprimeprodsq  12650  coprimeprodsq2  12651  pythagtriplem1  12658  pythagtriplem3  12660  pythagtriplem6  12663  pythagtriplem12  12668  pythagtriplem13  12669  pythagtriplem14  12670  pythagtriplem16  12672  pythagtriplem19  12675  pythagtrip  12676  pcmul  12694  pcdiv  12695  pcqcl  12699  pcgcd1  12721  pcgcd  12722  dvdsprmpweq  12728  difsqpwdvds  12731  pcfaclem  12742  unbendc  12895  strle3g  13010  ercpbl  13233  grpinvid1  13454  grpinvid2  13455  grpasscan1  13465  grpasscan2  13466  grpidrcan  13467  grpidlcan  13468  grpinvadd  13480  grpsubadd  13490  grppncan  13493  pwsinvg  13514  qussub  13643  subcmnd  13739  mulgass2  13890  dvrcan1  13972  dvrcan3  13973  rmodislmodlem  14182  rmodislmod  14183  islssm  14189  lsselg  14193  lspss  14231  lspssp  14235  lsslsp  14261  islidlm  14311  lidlnegcl  14317  lidlsubcl  14319  zndvds  14481  basgen  14622  clsss  14660  ntrin  14666  ntrcls0  14673  neiint  14687  neiss  14692  neipsm  14696  opnssneib  14698  innei  14705  restco  14716  iscnp  14741  cnconst2  14775  txcn  14817  psmetsym  14871  psmetlecl  14876  distspace  14877  xmetlecl  14909  xmetsym  14910  xblcntrps  14955  xblcntr  14956  blssec  14980  blpnfctr  14981  txmetcn  15061  cnmet  15072  dvid  15237  dvidre  15239  dvply1  15307  ptolemy  15366  sinq12gt0  15372  sincosq1eq  15381  rpcxpsub  15450  relogbexpap  15500  logbleb  15503  logblt  15504  rplogbcxp  15505  lgsval4  15567  lgsmod  15573  lgsne0  15585  lgsmulsqcoprm  15593  2lgsoddprmlem1  15652  structiedg0val  15709  lpvtx  15745