Theorem ad2antrr 492

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 481	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  496  ad5ant13  523  ad5ant23  526  simpll  531  simplll  539  simpllr  540  ad5ant123  1270  vtoclgft  2873  reupick  3517  ifeqeqxdc  3684  euotd  4390  frirrg  4490  ralxfrd  4603  nnsucpred  4759  foun  5653  f1oprg  5680  dffo4  5847  funopsn  5882  foeqcnvco  5986  fliftfun  5992  isotr  6012  riotass2  6057  ovmpodxf  6204  suppfnss  6487  suppcofn  6496  mpoxopoveq  6501  tfrlem1  6569  tfrlemibacc  6587  tfrlemibfn  6589  tfrlemi14d  6594  tfrexlem  6595  tfr1onlembacc  6603  tfr1onlembfn  6605  tfr1onlemres  6610  tfrcllembacc  6616  tfrcllembfn  6618  tfrcllemres  6623  frecabcl  6660  nnmordi  6779  eroprf  6892  mapsnd  6960  f1imaen2g  7070  pw2f1odclem  7124  xpen  7135  mapen  7136  mapdom1g  7137  mapxpen  7138  xpmapenlem  7139  phplem4dom  7153  nndomo  7155  phpm  7157  fidifsnen  7162  dif1enen  7174  fisbth  7177  fimax2gtrilemstep  7195  fimax2gtri  7196  eqsndc  7200  en2eqpr  7204  unsnfidcex  7217  unsnfidcel  7218  ssfirab  7234  fidcenumlemrks  7260  sbthlemi8  7271  fiuni  7302  2omap  7308  ordiso2  7365  updjud  7412  difinfsnlem  7429  ctssdclemn0  7440  ctssdccl  7441  ctssdc  7443  enumctlemm  7444  enumct  7445  nnnninfeq  7458  nninfisol  7463  enomnilem  7468  fodju0  7477  enmkvlem  7491  enwomnilem  7499  nninfwlpoimlemg  7505  pr1or2  7530  pr2cv1  7531  exmidfodomrlemim  7543  exmidontriimlem2  7568  exmidapne  7616  cc3  7624  dfplpq2  7711  nqpi  7735  nqnq0pi  7795  nq0nn  7799  elinp  7831  elnp1st2nd  7833  genprndl  7878  genprndu  7879  addnqprllem  7884  addnqprulem  7885  addnqprl  7886  addnqpru  7887  addlocpr  7893  nqprloc  7902  prmuloc  7923  mulnqprl  7925  mulnqpru  7926  mullocpr  7928  distrlem1prl  7939  distrlem1pru  7940  ltsopr  7953  ltexprlemopl  7958  ltexprlemopu  7960  ltexprlemloc  7964  ltexprlemrl  7967  ltexprlemru  7969  addcanprleml  7971  addcanprlemu  7972  recexprlemloc  7988  recexprlem1ssl  7990  recexprlem1ssu  7991  aptiprleml  7996  aptiprlemu  7997  archpr  8000  cauappcvgprlemm  8002  cauappcvgprlemopl  8003  cauappcvgprlemlol  8004  cauappcvgprlemladdfu  8011  cauappcvgprlemladdfl  8012  cauappcvgprlemladdru  8013  archrecpr  8021  caucvgprlemnkj  8023  caucvgprlemm  8025  caucvgprlemopl  8026  caucvgprlemlol  8027  caucvgprlemdisj  8031  caucvgprlemloc  8032  caucvgprlemladdfu  8034  caucvgprprlemnkltj  8046  caucvgprprlemnkeqj  8047  caucvgprprlemnjltk  8048  caucvgprprlemml  8051  caucvgprprlemopl  8054  caucvgprprlemlol  8055  caucvgprprlemdisj  8059  caucvgprprlemexbt  8063  caucvgprprlemexb  8064  caucvgprprlemaddq  8065  suplocexprlemru  8076  suplocexprlemloc  8078  suplocexprlemex  8079  suplocexprlemub  8080  suplocexprlemlub  8081  mulgt0sr  8135  caucvgsrlemcau  8150  caucvgsrlemoffcau  8155  caucvgsrlemoffres  8157  suplocsrlemb  8163  suplocsrlempr  8164  suplocsrlem  8165  axcaucvglemcau  8255  axcaucvglemres  8256  axpre-suploclemres  8258  axsuploc  8388  cnegexlem1  8491  cnegex  8494  apsym  8924  apcotr  8925  apadd1  8926  mulext1  8930  mulge0  8937  apti  8940  aprcl  8964  conjmulap  9049  lemulge11  9186  creui  9280  nndiv  9324  zaddcllemneg  9662  suprzclex  9723  eluzuzle  9909  infregelbex  9977  divfnzn  10000  qapne  10018  xrltso  10177  xnn0dcle  10183  xnn0letri  10184  xrre  10201  xrre3  10203  xaddf  10225  xaddval  10226  xpncan  10252  xleadd1a  10254  xltadd1  10257  xleaddadd  10268  ixxss12  10287  elioc2  10317  elico2  10318  elicc2  10319  fzm1  10485  fzneuz  10486  eluzgtdifelfzo  10593  elfzonelfzo  10626  exfzdc  10637  zsupcllemstep  10640  infssuzex  10644  suprzubdc  10649  nninfdcex  10650  zsupssdc  10651  qtri3or  10653  exbtwnzlemstep  10660  exbtwnzlemex  10662  exbtwnz  10663  modqid  10764  modqcyc2  10775  modqmuladd  10781  modqmuladdnn0  10783  modaddmodlo  10803  addmodlteq  10813  frecuzrdgrrn  10823  frec2uzrdg  10824  frecuzrdgsuc  10829  frecuzrdgsuctlem  10838  nninfinf  10858  seq3clss  10886  iseqf1olemqcl  10914  iseqf1olemnab  10916  iseqf1olemab  10917  iseqf1olemmo  10920  iseqf1olemqf1o  10921  iseqf1olemjpcl  10923  iseqf1olemqpcl  10924  seq3f1olemqsumk  10927  seq3f1olemqsum  10928  seq3f1olemp  10930  seq3f1oleml  10931  seq3f1o  10932  seqf1oglem1  10934  seqf1oglem2  10935  seqf1og  10936  seq3id3  10939  seqfeq4g  10946  ser3ge0  10951  exp3val  10956  expap0  10984  qsqeqor  11065  modqexp  11082  nn0ltexp2  11125  facndiv  11155  faclbnd  11157  bcval5  11179  hashunlem  11222  hashun  11223  hashprg  11227  fiprsshashgt1  11236  hashfacen  11262  hashf1lem1  11263  zfz1isolemiso  11269  zfz1isolem1  11270  seq3coll  11272  hashtpglem  11276  ccatcl  11339  ccatlen  11341  ccatvalfn  11347  ccatsymb  11348  ccatrn  11355  ccat2s1fstg  11394  swrdclg  11400  swrdspsleq  11417  pfxeq  11446  swrdswrd  11455  wrdind  11472  wrd2ind  11473  swrdccatin1  11475  swrdccatin2  11479  pfxccatin12  11483  pfxccat3  11484  swrdccat3b  11490  reuccatpfxs1  11497  ovshftex  11562  2shfti  11574  seq3shft  11581  cjap  11650  caucvgrelemcau  11724  cvg1nlemcau  11728  cvg1nlemres  11729  recvguniq  11739  resqrexlemdecn  11756  resqrexlemcalc3  11760  resqrexlemcvg  11763  resqrexlemoverl  11765  leabs  11818  absexpzap  11824  ltabs  11831  abslt  11832  absle  11833  maxleim  11949  maxabslemval  11952  fimaxre2  11971  minmax  11974  2zinfmin  11987  xrmaxiflemcl  11989  xrmaxifle  11990  xrmaxiflemab  11991  xrmaxiflemlub  11992  xrmaxiflemcom  11993  xrmaxltsup  12002  xrmaxadd  12005  xrminmax  12009  xrbdtri  12020  2clim  12045  climshftlemg  12046  climsqz  12079  climsqz2  12080  climrecvg1n  12092  climcvg1nlem  12093  serf0  12096  sumrbdclem  12122  fsum3cvg  12123  summodclem3  12125  summodclem2a  12126  summodclem2  12127  zsumdc  12129  fsum3  12132  isumss  12136  fisumss  12137  fsum3cvg3  12141  fsumcl2lem  12143  fsumadd  12151  fsumsplit  12152  sumsnf  12154  fsum2d  12180  fisum0diag2  12192  fsummulc2  12193  modfsummod  12203  fsumabs  12210  fsumrelem  12216  fsumiun  12222  geoisumr  12263  cvgratnnlemseq  12271  cvgratz  12277  mertenslemi1  12280  mertenslem2  12281  mertensabs  12282  prodrbdclem  12316  fproddccvg  12317  prodmodclem3  12320  prodmodclem2a  12321  zproddc  12324  fprodseq  12328  fprodntrivap  12329  fprodssdc  12335  fprodmul  12336  prodsnf  12337  fprodsplitdc  12341  fprodsplit  12342  fprodunsn  12349  fprodcl2lem  12350  fprodap0  12366  fprod2d  12368  fprodrec  12374  fprodap0f  12381  efcj  12418  efaddlem  12419  tanaddaplem  12483  sinltxirr  12506  nndivides  12542  dvdsext  12600  divalglemeunn  12666  divalglemex  12667  divalglemeuneg  12668  bitsfzolem  12699  bitsmod  12701  bitsinv1  12707  dvdsbnd  12711  bezoutlemnewy  12751  bezoutlemstep  12752  bezoutlemmain  12753  bezoutlemzz  12757  bezoutlemaz  12758  bezoutlembz  12759  bezoutlemeu  12762  bezoutlemle  12763  bezoutlemsup  12764  dfgcd3  12765  dfgcd2  12769  bezoutr1  12788  nnmindc  12789  nninfctlemfo  12795  dvdslcm  12825  lcmgcdlem  12833  qredeq  12852  qredeu  12853  divgcdcoprm0  12857  divgcdcoprmex  12858  cncongr1  12859  isprm2lem  12872  prmind2  12876  exprmfct  12894  prmdvdsfz  12895  isprm5lem  12897  prmexpb  12907  rpexp1i  12910  sqrt2irr  12918  sqne2sq  12933  nonsq  12963  phiprmpw  12978  eulerthlemrprm  12985  eulerthlema  12986  hashgcdeq  12996  phisum  12997  modprmn0modprm0  13013  pclemub  13044  pclemdc  13045  pcmul  13058  pcqmul  13060  pcxqcl  13069  pcdvdstr  13084  pcprmpw2  13090  difsqpwdvds  13095  pcmpt  13100  oddprmdvds  13111  prmpwdvds  13112  pockthg  13114  infpnlem1  13116  1arith  13124  4sqlem2  13146  4sqlemafi  13152  4sqlemffi  13153  4sqleminfi  13154  4sqlem11  13158  4sqlem13m  13160  4sqlem14  13161  4sqlem17  13164  4sqlem18  13165  ballotfilemi1  13223  ballotfilemii  13224  ballotfilemscl  13225  ballotfilemimin  13227  ballotfilemic  13228  ballotfilem1c  13229  ballotfilemsv  13231  ballotfilemsdom  13233  ballotfilemsima  13237  ennnfonelemg  13272  ennnfoneleminc  13280  ennnfonelemkh  13281  ennnfonelemhf1o  13282  ennnfonelemex  13283  ennnfonelemhom  13284  ennnfonelemfun  13286  ennnfonelemf1  13287  ennnfonelemrn  13288  ennnfonelemdm  13289  ennnfonelemnn0  13291  ennnfonelemim  13293  exmidunben  13295  ctinfomlemom  13296  ctinf  13299  ctiunctlemudc  13306  nninfdclemlt  13320  nninfdclemf1  13321  isstruct2r  13341  imasival  13604  sgrppropd  13705  mndpropd  13730  issubmnd  13732  mndissubm  13759  resmhm2b  13773  mhmeql  13776  gzsumwsubmcl  13778  gzsumwmhm  13780  gzsumcl  13781  grpinvnz  13853  mhmmnd  13896  mulgfng  13904  mulgz  13930  mulgnndir  13931  mulgnn0dir  13932  mulgneg2  13936  mulgass  13939  mhmmulg  13943  issubgrpd2  13970  issubg4m  13973  grpissubg  13974  isnsg3  13987  ghmpreima  14046  ghmnsgpreima  14049  ghmf1  14053  conjnmz  14059  conjnmzb  14060  eqgabl  14111  gzsumreidx  14118  gzsumsubmcl  14119  gzsummhm  14122  gsumvalfi  14129  gsumclfi  14136  gsumf1ofi  14137  gsummptfidmadd  14138  gsumsubmclfi  14140  prdsval  14150  prdssgrpd  14168  prdsidlem  14170  prdsmndd  14171  pws0g  14190  pwssub  14193  rngpropd  14229  issrg  14243  ringpropd  14316  ringinvnz1ne0  14327  dvdsrvald  14373  dvdsrd  14374  dvdsrtr  14381  unitgrp  14396  rhmopp  14456  aprnzr  14572  opprdrng  14593  lmodfopne  14635  lmodprop2d  14657  lssvacl  14674  lsslss  14690  lss1d  14692  lsspropdg  14740  rnglidlmcl  14789  lidlacl  14793  isridl  14813  gsumfsum  14895  znidomb  14965  znunit  14966  znrrg  14967  psrval  14973  mplsubgfilemcl  15013  mplsubgfileminv  15014  mplsubgfi  15015  tgdom  15096  neipsm  15178  tgrest  15193  cnfval  15218  cnpfval  15219  cnpval  15222  iscnp4  15242  cnpnei  15243  cnptopco  15246  cncnpi  15252  cncnp  15254  cnptopresti  15262  cnptoprest2  15264  cndis  15265  lmtopcnp  15274  txbasval  15291  neitx  15292  txcnp  15295  txcnmpt  15297  txcn  15299  imasnopn  15323  psmetres2  15357  isxmet2d  15372  xblss2ps  15428  xblss2  15429  blbas  15457  neibl  15515  metss2lem  15521  metrest  15530  xmettx  15534  metcnp3  15535  metcnp  15536  metcnp2  15537  metcnpi  15539  metcnpi2  15540  mulc1cncf  15613  cncfco  15615  mulcncflem  15631  mulcncf  15632  dedekindeulemuub  15641  dedekindeulemloc  15643  dedekindeulemlu  15645  dedekindeu  15647  suplociccreex  15648  suplociccex  15649  dedekindicclemuub  15650  dedekindicclemloc  15652  dedekindicclemlu  15654  dedekindicclemicc  15656  dedekindicc  15657  ivthinclemlopn  15660  ivthinclemlr  15661  ivthinclemuopn  15662  ivthinclemur  15663  ivthinclemloc  15665  ivthinc  15667  limcimolemlt  15688  limccnp2lem  15700  limccnp2cntop  15701  limccoap  15702  dvcj  15733  dvmptfsum  15749  dveflem  15750  plyf  15761  plyaddlem1  15771  plymullem1  15772  plycolemc  15782  plyco  15783  plycj  15785  dvply1  15789  dvply2g  15790  efltlemlt  15798  sin0pilem1  15805  sin0pilem2  15806  pilem3  15807  coseq0negpitopi  15860  abssinper  15870  cos02pilt1  15875  relogeftb  15889  logbgcd1irraplemexp  15993  logbgcd1irrap  15995  dvdsppwf1o  16017  mpodvdsmulf1o  16018  mersenne  16025  perfectlem2  16028  perfect  16029  lgsval  16037  lgsfvalg  16038  lgsfcl2  16039  lgsval2lem  16043  lgsmod  16059  lgsdilem  16060  lgsdir2lem4  16064  lgsdir2  16066  lgsdir  16068  lgsdilem2  16069  lgsdi  16070  lgsne0  16071  lgsdirnn0  16080  lgsdinn0  16081  gausslemma2dlem1a  16091  gausslemma2dlem1f1o  16093  lgsquadlem1  16110  lgsquadlem2  16111  lgsquad2lem2  16115  2lgslem1a1  16119  2lgslem1a  16121  2sqlem5  16152  2sqlem6  16153  2sqlem7  16154  2sqlem9  16157  2sqlem10  16158  umgrnloopv  16269  uhgr2edg  16361  upgredginwlk  16511  clwwlkccatlem  16555  eupth2lem3lem3fi  16625  eupth2lem3lem4fi  16628  eupth2lemsfi  16633  depindlem3  16663  bj-findis  16919  pwle2  16942  pwf1oexmid  16943  pw1nct  16947  nnsf  16953  peano4nninf  16954  nninfall  16957  nninfsellemeq  16962  nninfsellemeqinf  16964  nnnninfex  16970  nninfnfiinf  16971  qdencn  16977  refeq  16978  trilpolemeq1  16994  trilpolemlt1  16995  trirec0  16998  nconstwlpolemgt0  17019  nconstwlpolem  17020  neapmkvlem  17022