Theorem ad2antrr 488

Description: Deduction adding two conjuncts to antecedent. (Contributed by NM, 19-Oct-1999.) (Proof shortened by Wolf Lammen, 20-Nov-2012.)

Hypothesis

Ref	Expression
ad2ant.1	⊢ (𝜑 → 𝜓)

Assertion

Ref	Expression
ad2antrr	⊢ (((𝜑 ∧ 𝜒) ∧ 𝜃) → 𝜓)

Proof of Theorem ad2antrr

Step	Hyp	Ref	Expression
1		ad2ant.1	. . 3 ⊢ (𝜑 → 𝜓)
2	1	adantr 276	. 2 ⊢ ((𝜑 ∧ 𝜃) → 𝜓)
3	2	adantlr 477	1 ⊢ (((𝜑 ∧ 𝜒) ∧ 𝜃) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is referenced by:  ad3antrrr  492  ad5ant13  519  ad5ant23  522  simpll  527  simplll  533  simpllr  534  vtoclgft  2788  reupick  3420  euotd  4255  frirrg  4351  ralxfrd  4463  nnsucpred  4617  foun  5481  f1oprg  5506  dffo4  5665  foeqcnvco  5791  fliftfun  5797  isotr  5817  riotass2  5857  ovmpodxf  6000  mpoxopoveq  6241  tfrlem1  6309  tfrlemibacc  6327  tfrlemibfn  6329  tfrlemi14d  6334  tfrexlem  6335  tfr1onlembacc  6343  tfr1onlembfn  6345  tfr1onlemres  6350  tfrcllembacc  6356  tfrcllembfn  6358  tfrcllemres  6363  frecabcl  6400  nnmordi  6517  eroprf  6628  f1imaen2g  6793  xpen  6845  mapen  6846  mapdom1g  6847  mapxpen  6848  xpmapenlem  6849  phplem4dom  6862  nndomo  6864  phpm  6865  fidifsnen  6870  dif1enen  6880  fisbth  6883  fimax2gtrilemstep  6900  fimax2gtri  6901  en2eqpr  6907  unsnfidcex  6919  unsnfidcel  6920  ssfirab  6933  fidcenumlemrks  6952  sbthlemi8  6963  fiuni  6977  ordiso2  7034  updjud  7081  difinfsnlem  7098  ctssdclemn0  7109  ctssdccl  7110  ctssdc  7112  enumctlemm  7113  enumct  7114  nnnninfeq  7126  nninfisol  7131  enomnilem  7136  fodju0  7145  enmkvlem  7159  enwomnilem  7167  nninfwlpoimlemg  7173  exmidfodomrlemim  7200  exmidontriimlem2  7221  exmidapne  7259  cc3  7267  dfplpq2  7353  nqpi  7377  nqnq0pi  7437  nq0nn  7441  elinp  7473  elnp1st2nd  7475  genprndl  7520  genprndu  7521  addnqprllem  7526  addnqprulem  7527  addnqprl  7528  addnqpru  7529  addlocpr  7535  nqprloc  7544  prmuloc  7565  mulnqprl  7567  mulnqpru  7568  mullocpr  7570  distrlem1prl  7581  distrlem1pru  7582  ltsopr  7595  ltexprlemopl  7600  ltexprlemopu  7602  ltexprlemloc  7606  ltexprlemrl  7609  ltexprlemru  7611  addcanprleml  7613  addcanprlemu  7614  recexprlemloc  7630  recexprlem1ssl  7632  recexprlem1ssu  7633  aptiprleml  7638  aptiprlemu  7639  archpr  7642  cauappcvgprlemm  7644  cauappcvgprlemopl  7645  cauappcvgprlemlol  7646  cauappcvgprlemladdfu  7653  cauappcvgprlemladdfl  7654  cauappcvgprlemladdru  7655  archrecpr  7663  caucvgprlemnkj  7665  caucvgprlemm  7667  caucvgprlemopl  7668  caucvgprlemlol  7669  caucvgprlemdisj  7673  caucvgprlemloc  7674  caucvgprlemladdfu  7676  caucvgprprlemnkltj  7688  caucvgprprlemnkeqj  7689  caucvgprprlemnjltk  7690  caucvgprprlemml  7693  caucvgprprlemopl  7696  caucvgprprlemlol  7697  caucvgprprlemdisj  7701  caucvgprprlemexbt  7705  caucvgprprlemexb  7706  caucvgprprlemaddq  7707  suplocexprlemru  7718  suplocexprlemloc  7720  suplocexprlemex  7721  suplocexprlemub  7722  suplocexprlemlub  7723  mulgt0sr  7777  caucvgsrlemcau  7792  caucvgsrlemoffcau  7797  caucvgsrlemoffres  7799  suplocsrlemb  7805  suplocsrlempr  7806  suplocsrlem  7807  axcaucvglemcau  7897  axcaucvglemres  7898  axpre-suploclemres  7900  axsuploc  8030  cnegexlem1  8132  cnegex  8135  apsym  8563  apcotr  8564  apadd1  8565  mulext1  8569  mulge0  8576  apti  8579  aprcl  8603  conjmulap  8686  lemulge11  8823  creui  8917  nndiv  8960  zaddcllemneg  9292  suprzclex  9351  eluzuzle  9536  infregelbex  9598  divfnzn  9621  qapne  9639  xrltso  9796  xnn0dcle  9802  xnn0letri  9803  xrre  9820  xrre3  9822  xaddf  9844  xaddval  9845  xpncan  9871  xleadd1a  9873  xltadd1  9876  xleaddadd  9887  ixxss12  9906  elioc2  9936  elico2  9937  elicc2  9938  fzm1  10100  fzneuz  10101  eluzgtdifelfzo  10197  elfzonelfzo  10230  exfzdc  10240  qtri3or  10243  exbtwnzlemstep  10248  exbtwnzlemex  10250  exbtwnz  10251  modqid  10349  modqcyc2  10360  modqmuladd  10366  modqmuladdnn0  10368  modaddmodlo  10388  addmodlteq  10398  frecuzrdgrrn  10408  frec2uzrdg  10409  frecuzrdgsuc  10414  frecuzrdgsuctlem  10423  seq3clss  10467  iseqf1olemqcl  10486  iseqf1olemnab  10488  iseqf1olemab  10489  iseqf1olemmo  10492  iseqf1olemqf1o  10493  iseqf1olemjpcl  10495  iseqf1olemqpcl  10496  seq3f1olemqsumk  10499  seq3f1olemqsum  10500  seq3f1olemp  10502  seq3f1oleml  10503  seq3f1o  10504  seq3id3  10507  ser3ge0  10517  exp3val  10522  expap0  10550  qsqeqor  10631  modqexp  10647  nn0ltexp2  10689  facndiv  10719  faclbnd  10721  bcval5  10743  hashunlem  10784  hashun  10785  hashprg  10788  fiprsshashgt1  10797  hashfacen  10816  zfz1isolemiso  10819  zfz1isolem1  10820  seq3coll  10822  ovshftex  10828  2shfti  10840  seq3shft  10847  cjap  10915  caucvgrelemcau  10989  cvg1nlemcau  10993  cvg1nlemres  10994  recvguniq  11004  resqrexlemdecn  11021  resqrexlemcalc3  11025  resqrexlemcvg  11028  resqrexlemoverl  11030  leabs  11083  absexpzap  11089  ltabs  11096  abslt  11097  absle  11098  maxleim  11214  maxabslemval  11217  fimaxre2  11235  minmax  11238  2zinfmin  11251  xrmaxiflemcl  11253  xrmaxifle  11254  xrmaxiflemab  11255  xrmaxiflemlub  11256  xrmaxiflemcom  11257  xrmaxltsup  11266  xrmaxadd  11269  xrminmax  11273  xrbdtri  11284  2clim  11309  climshftlemg  11310  climsqz  11343  climsqz2  11344  climrecvg1n  11356  climcvg1nlem  11357  serf0  11360  sumrbdclem  11385  fsum3cvg  11386  summodclem3  11388  summodclem2a  11389  summodclem2  11390  zsumdc  11392  fsum3  11395  isumss  11399  fisumss  11400  fsum3cvg3  11404  fsumcl2lem  11406  fsumadd  11414  fsumsplit  11415  sumsnf  11417  fsum2d  11443  fisum0diag2  11455  fsummulc2  11456  modfsummod  11466  fsumabs  11473  fsumrelem  11479  fsumiun  11485  geoisumr  11526  cvgratnnlemseq  11534  cvgratz  11540  mertenslemi1  11543  mertenslem2  11544  mertensabs  11545  prodrbdclem  11579  fproddccvg  11580  prodmodclem3  11583  prodmodclem2a  11584  zproddc  11587  fprodseq  11591  fprodntrivap  11592  fprodssdc  11598  fprodmul  11599  prodsnf  11600  fprodsplitdc  11604  fprodsplit  11605  fprodunsn  11612  fprodcl2lem  11613  fprodap0  11629  fprod2d  11631  fprodrec  11637  fprodap0f  11644  efcj  11681  efaddlem  11682  tanaddaplem  11746  nndivides  11804  dvdsext  11861  divalglemeunn  11926  divalglemex  11927  divalglemeuneg  11928  zsupcllemstep  11946  infssuzex  11950  suprzubdc  11953  nninfdcex  11954  zsupssdc  11955  dvdsbnd  11957  bezoutlemnewy  11997  bezoutlemstep  11998  bezoutlemmain  11999  bezoutlemzz  12003  bezoutlemaz  12004  bezoutlembz  12005  bezoutlemeu  12008  bezoutlemle  12009  bezoutlemsup  12010  dfgcd3  12011  dfgcd2  12015  bezoutr1  12034  nnmindc  12035  dvdslcm  12069  lcmgcdlem  12077  qredeq  12096  qredeu  12097  divgcdcoprm0  12101  divgcdcoprmex  12102  cncongr1  12103  isprm2lem  12116  prmind2  12120  exprmfct  12138  prmdvdsfz  12139  isprm5lem  12141  prmexpb  12151  rpexp1i  12154  sqrt2irr  12162  sqne2sq  12177  nonsq  12207  phiprmpw  12222  eulerthlemrprm  12229  eulerthlema  12230  hashgcdeq  12239  phisum  12240  modprmn0modprm0  12256  pclemub  12287  pclemdc  12288  pcmul  12301  pcqmul  12303  pcdvdstr  12326  pcprmpw2  12332  difsqpwdvds  12337  pcmpt  12341  oddprmdvds  12352  prmpwdvds  12353  pockthg  12355  infpnlem1  12357  1arith  12365  4sqlem2  12387  ennnfonelemg  12404  ennnfoneleminc  12412  ennnfonelemkh  12413  ennnfonelemhf1o  12414  ennnfonelemex  12415  ennnfonelemhom  12416  ennnfonelemfun  12418  ennnfonelemf1  12419  ennnfonelemrn  12420  ennnfonelemdm  12421  ennnfonelemnn0  12423  ennnfonelemim  12425  exmidunben  12427  ctinfomlemom  12428  ctinf  12431  ctiunctlemudc  12438  nninfdclemlt  12452  nninfdclemf1  12453  isstruct2r  12473  imasival  12727  mndpropd  12841  issubmnd  12843  mndissubm  12866  mhmeql  12876  grpinvnz  12941  mhmmnd  12980  mulgfng  12987  mulgz  13011  mulgnndir  13012  mulgnn0dir  13013  mulgneg2  13017  mulgass  13020  mhmmulg  13024  issubgrpd2  13050  issubg4m  13053  grpissubg  13054  isnsg3  13067  issrg  13148  ringpropd  13217  ringinvnz1ne0  13226  dvdsrvald  13262  dvdsrd  13263  dvdsrtr  13270  unitgrp  13285  lmodfopne  13416  lmodprop2d  13438  tgdom  13575  neipsm  13657  tgrest  13672  cnfval  13697  cnpfval  13698  cnpval  13701  iscnp4  13721  cnpnei  13722  cnptopco  13725  cncnpi  13731  cncnp  13733  cnptopresti  13741  cnptoprest2  13743  cndis  13744  lmtopcnp  13753  txbasval  13770  neitx  13771  txcnp  13774  txcnmpt  13776  txcn  13778  imasnopn  13802  psmetres2  13836  isxmet2d  13851  xblss2ps  13907  xblss2  13908  blbas  13936  neibl  13994  metss2lem  14000  metrest  14009  xmettx  14013  metcnp3  14014  metcnp  14015  metcnp2  14016  metcnpi  14018  metcnpi2  14019  mulc1cncf  14079  cncfco  14081  mulcncflem  14093  mulcncf  14094  dedekindeulemuub  14098  dedekindeulemloc  14100  dedekindeulemlu  14102  dedekindeu  14104  suplociccreex  14105  suplociccex  14106  dedekindicclemuub  14107  dedekindicclemloc  14109  dedekindicclemlu  14111  dedekindicclemicc  14113  dedekindicc  14114  ivthinclemlopn  14117  ivthinclemlr  14118  ivthinclemuopn  14119  ivthinclemur  14120  ivthinclemloc  14122  ivthinc  14124  limcimolemlt  14136  limccnp2lem  14148  limccnp2cntop  14149  limccoap  14150  dvcj  14176  dveflem  14190  efltlemlt  14198  sin0pilem1  14205  sin0pilem2  14206  pilem3  14207  coseq0negpitopi  14260  abssinper  14270  cos02pilt1  14275  relogeftb  14289  logbgcd1irraplemexp  14389  logbgcd1irrap  14391  lgsval  14408  lgsfvalg  14409  lgsfcl2  14410  lgsval2lem  14414  lgsmod  14430  lgsdilem  14431  lgsdir2lem4  14435  lgsdir2  14437  lgsdir  14439  lgsdilem2  14440  lgsdi  14441  lgsne0  14442  lgsdirnn0  14451  lgsdinn0  14452  2sqlem5  14469  2sqlem6  14470  2sqlem7  14471  2sqlem9  14474  2sqlem10  14475  bj-findis  14734  pwle2  14751  pwf1oexmid  14752  pw1nct  14755  nnsf  14757  peano4nninf  14758  nninfall  14761  nninfsellemeq  14766  nninfsellemeqinf  14768  qdencn  14778  refeq  14779  trilpolemeq1  14791  trilpolemlt1  14792  trirec0  14795  nconstwlpolemgt0  14814  nconstwlpolem  14815  neapmkvlem  14817