Theorem ad2antrr 480

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 274	. 2 ⊢ ((𝜑 ∧ 𝜃) → 𝜓)
3	2	adantlr 469	1 ⊢ (((𝜑 ∧ 𝜒) ∧ 𝜃) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 103

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

This theorem is referenced by:  ad3antrrr  484  ad5ant13  511  ad5ant23  514  simpll  519  simplll  523  simpllr  524  vtoclgft  2739  reupick  3365  euotd  4184  frirrg  4280  ralxfrd  4391  nnsucpred  4538  foun  5394  f1oprg  5419  dffo4  5576  foeqcnvco  5699  fliftfun  5705  isotr  5725  riotass2  5764  ovmpodxf  5904  mpoxopoveq  6145  tfrlem1  6213  tfrlemibacc  6231  tfrlemibfn  6233  tfrlemi14d  6238  tfrexlem  6239  tfr1onlembacc  6247  tfr1onlembfn  6249  tfr1onlemres  6254  tfrcllembacc  6260  tfrcllembfn  6262  tfrcllemres  6267  frecabcl  6304  nnmordi  6420  eroprf  6530  f1imaen2g  6695  xpen  6747  mapen  6748  mapdom1g  6749  mapxpen  6750  xpmapenlem  6751  phplem4dom  6764  nndomo  6766  phpm  6767  fidifsnen  6772  dif1enen  6782  fisbth  6785  fimax2gtrilemstep  6802  fimax2gtri  6803  en2eqpr  6809  unsnfidcex  6816  unsnfidcel  6817  ssfirab  6830  fidcenumlemrks  6849  sbthlemi8  6860  fiuni  6874  ordiso2  6928  updjud  6975  difinfsnlem  6992  ctssdclemn0  7003  ctssdccl  7004  ctssdc  7006  enumctlemm  7007  enumct  7008  enomnilem  7018  fodju0  7027  enmkvlem  7043  enwomnilem  7050  exmidfodomrlemim  7074  cc3  7100  dfplpq2  7186  nqpi  7210  nqnq0pi  7270  nq0nn  7274  elinp  7306  elnp1st2nd  7308  genprndl  7353  genprndu  7354  addnqprllem  7359  addnqprulem  7360  addnqprl  7361  addnqpru  7362  addlocpr  7368  nqprloc  7377  prmuloc  7398  mulnqprl  7400  mulnqpru  7401  mullocpr  7403  distrlem1prl  7414  distrlem1pru  7415  ltsopr  7428  ltexprlemopl  7433  ltexprlemopu  7435  ltexprlemloc  7439  ltexprlemrl  7442  ltexprlemru  7444  addcanprleml  7446  addcanprlemu  7447  recexprlemloc  7463  recexprlem1ssl  7465  recexprlem1ssu  7466  aptiprleml  7471  aptiprlemu  7472  archpr  7475  cauappcvgprlemm  7477  cauappcvgprlemopl  7478  cauappcvgprlemlol  7479  cauappcvgprlemladdfu  7486  cauappcvgprlemladdfl  7487  cauappcvgprlemladdru  7488  archrecpr  7496  caucvgprlemnkj  7498  caucvgprlemm  7500  caucvgprlemopl  7501  caucvgprlemlol  7502  caucvgprlemdisj  7506  caucvgprlemloc  7507  caucvgprlemladdfu  7509  caucvgprprlemnkltj  7521  caucvgprprlemnkeqj  7522  caucvgprprlemnjltk  7523  caucvgprprlemml  7526  caucvgprprlemopl  7529  caucvgprprlemlol  7530  caucvgprprlemdisj  7534  caucvgprprlemexbt  7538  caucvgprprlemexb  7539  caucvgprprlemaddq  7540  suplocexprlemru  7551  suplocexprlemloc  7553  suplocexprlemex  7554  suplocexprlemub  7555  suplocexprlemlub  7556  mulgt0sr  7610  caucvgsrlemcau  7625  caucvgsrlemoffcau  7630  caucvgsrlemoffres  7632  suplocsrlemb  7638  suplocsrlempr  7639  suplocsrlem  7640  axcaucvglemcau  7730  axcaucvglemres  7731  axpre-suploclemres  7733  axsuploc  7861  cnegexlem1  7961  cnegex  7964  apsym  8392  apcotr  8393  apadd1  8394  mulext1  8398  mulge0  8405  apti  8408  aprcl  8432  conjmulap  8513  lemulge11  8648  creui  8742  nndiv  8785  zaddcllemneg  9117  suprzclex  9173  eluzuzle  9358  divfnzn  9440  qapne  9458  xrltso  9612  xrre  9633  xrre3  9635  xaddf  9657  xaddval  9658  xpncan  9684  xleadd1a  9686  xltadd1  9689  xleaddadd  9700  ixxss12  9719  elioc2  9749  elico2  9750  elicc2  9751  fzm1  9911  fzneuz  9912  eluzgtdifelfzo  10005  elfzonelfzo  10038  exfzdc  10048  qtri3or  10051  exbtwnzlemstep  10056  exbtwnzlemex  10058  exbtwnz  10059  modqid  10153  modqcyc2  10164  modqmuladd  10170  modqmuladdnn0  10172  modaddmodlo  10192  addmodlteq  10202  frecuzrdgrrn  10212  frec2uzrdg  10213  frecuzrdgsuc  10218  frecuzrdgsuctlem  10227  seq3clss  10271  iseqf1olemqcl  10290  iseqf1olemnab  10292  iseqf1olemab  10293  iseqf1olemmo  10296  iseqf1olemqf1o  10297  iseqf1olemjpcl  10299  iseqf1olemqpcl  10300  seq3f1olemqsumk  10303  seq3f1olemqsum  10304  seq3f1olemp  10306  seq3f1oleml  10307  seq3f1o  10308  seq3id3  10311  ser3ge0  10321  exp3val  10326  expap0  10354  facndiv  10517  faclbnd  10519  bcval5  10541  hashunlem  10582  hashun  10583  hashprg  10586  fiprsshashgt1  10595  hashfacen  10611  zfz1isolemiso  10614  zfz1isolem1  10615  seq3coll  10617  ovshftex  10623  2shfti  10635  seq3shft  10642  cjap  10710  caucvgrelemcau  10784  cvg1nlemcau  10788  cvg1nlemres  10789  recvguniq  10799  resqrexlemdecn  10816  resqrexlemcalc3  10820  resqrexlemcvg  10823  resqrexlemoverl  10825  leabs  10878  absexpzap  10884  ltabs  10891  abslt  10892  absle  10893  maxleim  11009  maxabslemval  11012  fimaxre2  11030  minmax  11033  xrmaxiflemcl  11046  xrmaxifle  11047  xrmaxiflemab  11048  xrmaxiflemlub  11049  xrmaxiflemcom  11050  xrmaxltsup  11059  xrmaxadd  11062  xrminmax  11066  xrbdtri  11077  2clim  11102  climshftlemg  11103  climsqz  11136  climsqz2  11137  climrecvg1n  11149  climcvg1nlem  11150  serf0  11153  sumrbdclem  11178  fsum3cvg  11179  summodclem3  11181  summodclem2a  11182  summodclem2  11183  zsumdc  11185  fsum3  11188  isumss  11192  fisumss  11193  fsum3cvg3  11197  fsumcl2lem  11199  fsumadd  11207  fsumsplit  11208  sumsnf  11210  fsum2d  11236  fisum0diag2  11248  fsummulc2  11249  modfsummod  11259  fsumabs  11266  fsumrelem  11272  fsumiun  11278  geoisumr  11319  cvgratnnlemseq  11327  cvgratz  11333  mertenslemi1  11336  mertenslem2  11337  mertensabs  11338  prodrbdclem  11372  fproddccvg  11373  prodmodclem3  11376  prodmodclem2a  11377  zproddc  11380  fprodseq  11384  efcj  11416  efaddlem  11417  tanaddaplem  11481  nndivides  11536  dvdsext  11589  divalglemeunn  11654  divalglemex  11655  divalglemeuneg  11656  zsupcllemstep  11674  infssuzex  11678  dvdsbnd  11681  bezoutlemnewy  11720  bezoutlemstep  11721  bezoutlemmain  11722  bezoutlemzz  11726  bezoutlemaz  11727  bezoutlembz  11728  bezoutlemeu  11731  bezoutlemle  11732  bezoutlemsup  11733  dfgcd3  11734  dfgcd2  11738  bezoutr1  11757  dvdslcm  11786  lcmgcdlem  11794  qredeq  11813  qredeu  11814  divgcdcoprm0  11818  divgcdcoprmex  11819  cncongr1  11820  isprm2lem  11833  prmind2  11837  exprmfct  11854  prmdvdsfz  11855  prmexpb  11865  rpexp1i  11868  sqrt2irr  11876  sqne2sq  11891  nonsq  11921  phiprmpw  11934  hashgcdeq  11940  ennnfonelemg  11952  ennnfoneleminc  11960  ennnfonelemkh  11961  ennnfonelemhf1o  11962  ennnfonelemex  11963  ennnfonelemhom  11964  ennnfonelemfun  11966  ennnfonelemf1  11967  ennnfonelemrn  11968  ennnfonelemdm  11969  ennnfonelemnn0  11971  ennnfonelemim  11973  exmidunben  11975  ctinfomlemom  11976  ctinf  11979  ctiunctlemudc  11986  isstruct2r  12009  tgdom  12280  neipsm  12362  tgrest  12377  cnfval  12402  cnpfval  12403  cnpval  12406  iscnp4  12426  cnpnei  12427  cnptopco  12430  cncnpi  12436  cncnp  12438  cnptopresti  12446  cnptoprest2  12448  cndis  12449  lmtopcnp  12458  txbasval  12475  neitx  12476  txcnp  12479  txcnmpt  12481  txcn  12483  imasnopn  12507  psmetres2  12541  isxmet2d  12556  xblss2ps  12612  xblss2  12613  blbas  12641  neibl  12699  metss2lem  12705  metrest  12714  xmettx  12718  metcnp3  12719  metcnp  12720  metcnp2  12721  metcnpi  12723  metcnpi2  12724  mulc1cncf  12784  cncfco  12786  mulcncflem  12798  mulcncf  12799  dedekindeulemuub  12803  dedekindeulemloc  12805  dedekindeulemlu  12807  dedekindeu  12809  suplociccreex  12810  suplociccex  12811  dedekindicclemuub  12812  dedekindicclemloc  12814  dedekindicclemlu  12816  dedekindicclemicc  12818  dedekindicc  12819  ivthinclemlopn  12822  ivthinclemlr  12823  ivthinclemuopn  12824  ivthinclemur  12825  ivthinclemloc  12827  ivthinc  12829  limcimolemlt  12841  limccnp2lem  12853  limccnp2cntop  12854  limccoap  12855  dvcj  12881  dveflem  12895  efltlemlt  12903  sin0pilem1  12910  sin0pilem2  12911  pilem3  12912  coseq0negpitopi  12965  abssinper  12975  cos02pilt1  12980  relogeftb  12994  logbgcd1irraplemexp  13093  logbgcd1irrap  13095  bj-findis  13348  pwle2  13366  pwf1oexmid  13367  pw1nct  13371  nnsf  13374  peano4nninf  13375  nninfalllemn  13377  nninfall  13379  nninfsellemeq  13385  nninfsellemeqinf  13387  qdencn  13397  refeq  13398  trilpolemeq1  13408  trilpolemlt1  13409  trirec0  13412  neapmkvlem  13424