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  2762  reupick  3392  euotd  4217  frirrg  4313  ralxfrd  4425  nnsucpred  4579  foun  5436  f1oprg  5461  dffo4  5618  foeqcnvco  5743  fliftfun  5749  isotr  5769  riotass2  5809  ovmpodxf  5949  mpoxopoveq  6190  tfrlem1  6258  tfrlemibacc  6276  tfrlemibfn  6278  tfrlemi14d  6283  tfrexlem  6284  tfr1onlembacc  6292  tfr1onlembfn  6294  tfr1onlemres  6299  tfrcllembacc  6305  tfrcllembfn  6307  tfrcllemres  6312  frecabcl  6349  nnmordi  6466  eroprf  6576  f1imaen2g  6741  xpen  6793  mapen  6794  mapdom1g  6795  mapxpen  6796  xpmapenlem  6797  phplem4dom  6810  nndomo  6812  phpm  6813  fidifsnen  6818  dif1enen  6828  fisbth  6831  fimax2gtrilemstep  6848  fimax2gtri  6849  en2eqpr  6855  unsnfidcex  6867  unsnfidcel  6868  ssfirab  6881  fidcenumlemrks  6900  sbthlemi8  6911  fiuni  6925  ordiso2  6982  updjud  7029  difinfsnlem  7046  ctssdclemn0  7057  ctssdccl  7058  ctssdc  7060  enumctlemm  7061  enumct  7062  nnnninfeq  7074  nninfisol  7079  enomnilem  7084  fodju0  7093  enmkvlem  7107  enwomnilem  7115  exmidfodomrlemim  7139  exmidontriimlem2  7160  cc3  7191  dfplpq2  7277  nqpi  7301  nqnq0pi  7361  nq0nn  7365  elinp  7397  elnp1st2nd  7399  genprndl  7444  genprndu  7445  addnqprllem  7450  addnqprulem  7451  addnqprl  7452  addnqpru  7453  addlocpr  7459  nqprloc  7468  prmuloc  7489  mulnqprl  7491  mulnqpru  7492  mullocpr  7494  distrlem1prl  7505  distrlem1pru  7506  ltsopr  7519  ltexprlemopl  7524  ltexprlemopu  7526  ltexprlemloc  7530  ltexprlemrl  7533  ltexprlemru  7535  addcanprleml  7537  addcanprlemu  7538  recexprlemloc  7554  recexprlem1ssl  7556  recexprlem1ssu  7557  aptiprleml  7562  aptiprlemu  7563  archpr  7566  cauappcvgprlemm  7568  cauappcvgprlemopl  7569  cauappcvgprlemlol  7570  cauappcvgprlemladdfu  7577  cauappcvgprlemladdfl  7578  cauappcvgprlemladdru  7579  archrecpr  7587  caucvgprlemnkj  7589  caucvgprlemm  7591  caucvgprlemopl  7592  caucvgprlemlol  7593  caucvgprlemdisj  7597  caucvgprlemloc  7598  caucvgprlemladdfu  7600  caucvgprprlemnkltj  7612  caucvgprprlemnkeqj  7613  caucvgprprlemnjltk  7614  caucvgprprlemml  7617  caucvgprprlemopl  7620  caucvgprprlemlol  7621  caucvgprprlemdisj  7625  caucvgprprlemexbt  7629  caucvgprprlemexb  7630  caucvgprprlemaddq  7631  suplocexprlemru  7642  suplocexprlemloc  7644  suplocexprlemex  7645  suplocexprlemub  7646  suplocexprlemlub  7647  mulgt0sr  7701  caucvgsrlemcau  7716  caucvgsrlemoffcau  7721  caucvgsrlemoffres  7723  suplocsrlemb  7729  suplocsrlempr  7730  suplocsrlem  7731  axcaucvglemcau  7821  axcaucvglemres  7822  axpre-suploclemres  7824  axsuploc  7953  cnegexlem1  8055  cnegex  8058  apsym  8486  apcotr  8487  apadd1  8488  mulext1  8492  mulge0  8499  apti  8502  aprcl  8526  conjmulap  8607  lemulge11  8743  creui  8837  nndiv  8880  zaddcllemneg  9212  suprzclex  9268  eluzuzle  9453  infregelbex  9515  divfnzn  9537  qapne  9555  xrltso  9710  xrre  9731  xrre3  9733  xaddf  9755  xaddval  9756  xpncan  9782  xleadd1a  9784  xltadd1  9787  xleaddadd  9798  ixxss12  9817  elioc2  9847  elico2  9848  elicc2  9849  fzm1  10009  fzneuz  10010  eluzgtdifelfzo  10106  elfzonelfzo  10139  exfzdc  10149  qtri3or  10152  exbtwnzlemstep  10157  exbtwnzlemex  10159  exbtwnz  10160  modqid  10258  modqcyc2  10269  modqmuladd  10275  modqmuladdnn0  10277  modaddmodlo  10297  addmodlteq  10307  frecuzrdgrrn  10317  frec2uzrdg  10318  frecuzrdgsuc  10323  frecuzrdgsuctlem  10332  seq3clss  10376  iseqf1olemqcl  10395  iseqf1olemnab  10397  iseqf1olemab  10398  iseqf1olemmo  10401  iseqf1olemqf1o  10402  iseqf1olemjpcl  10404  iseqf1olemqpcl  10405  seq3f1olemqsumk  10408  seq3f1olemqsum  10409  seq3f1olemp  10411  seq3f1oleml  10412  seq3f1o  10413  seq3id3  10416  ser3ge0  10426  exp3val  10431  expap0  10459  modqexp  10554  nn0ltexp2  10596  facndiv  10625  faclbnd  10627  bcval5  10649  hashunlem  10690  hashun  10691  hashprg  10694  fiprsshashgt1  10703  hashfacen  10719  zfz1isolemiso  10722  zfz1isolem1  10723  seq3coll  10725  ovshftex  10731  2shfti  10743  seq3shft  10750  cjap  10818  caucvgrelemcau  10892  cvg1nlemcau  10896  cvg1nlemres  10897  recvguniq  10907  resqrexlemdecn  10924  resqrexlemcalc3  10928  resqrexlemcvg  10931  resqrexlemoverl  10933  leabs  10986  absexpzap  10992  ltabs  10999  abslt  11000  absle  11001  maxleim  11117  maxabslemval  11120  fimaxre2  11138  minmax  11141  xrmaxiflemcl  11154  xrmaxifle  11155  xrmaxiflemab  11156  xrmaxiflemlub  11157  xrmaxiflemcom  11158  xrmaxltsup  11167  xrmaxadd  11170  xrminmax  11174  xrbdtri  11185  2clim  11210  climshftlemg  11211  climsqz  11244  climsqz2  11245  climrecvg1n  11257  climcvg1nlem  11258  serf0  11261  sumrbdclem  11286  fsum3cvg  11287  summodclem3  11289  summodclem2a  11290  summodclem2  11291  zsumdc  11293  fsum3  11296  isumss  11300  fisumss  11301  fsum3cvg3  11305  fsumcl2lem  11307  fsumadd  11315  fsumsplit  11316  sumsnf  11318  fsum2d  11344  fisum0diag2  11356  fsummulc2  11357  modfsummod  11367  fsumabs  11374  fsumrelem  11380  fsumiun  11386  geoisumr  11427  cvgratnnlemseq  11435  cvgratz  11441  mertenslemi1  11444  mertenslem2  11445  mertensabs  11446  prodrbdclem  11480  fproddccvg  11481  prodmodclem3  11484  prodmodclem2a  11485  zproddc  11488  fprodseq  11492  fprodntrivap  11493  fprodssdc  11499  fprodmul  11500  prodsnf  11501  fprodsplitdc  11505  fprodsplit  11506  fprodunsn  11513  fprodcl2lem  11514  fprodap0  11530  fprod2d  11532  fprodrec  11538  fprodap0f  11545  efcj  11582  efaddlem  11583  tanaddaplem  11647  nndivides  11705  dvdsext  11760  divalglemeunn  11825  divalglemex  11826  divalglemeuneg  11827  zsupcllemstep  11845  infssuzex  11849  suprzubdc  11852  nninfdcex  11853  zsupssdc  11854  dvdsbnd  11856  bezoutlemnewy  11896  bezoutlemstep  11897  bezoutlemmain  11898  bezoutlemzz  11902  bezoutlemaz  11903  bezoutlembz  11904  bezoutlemeu  11907  bezoutlemle  11908  bezoutlemsup  11909  dfgcd3  11910  dfgcd2  11914  bezoutr1  11933  dvdslcm  11962  lcmgcdlem  11970  qredeq  11989  qredeu  11990  divgcdcoprm0  11994  divgcdcoprmex  11995  cncongr1  11996  isprm2lem  12009  prmind2  12013  exprmfct  12031  prmdvdsfz  12032  prmexpb  12042  rpexp1i  12045  sqrt2irr  12053  sqne2sq  12068  nonsq  12098  phiprmpw  12113  eulerthlemrprm  12120  eulerthlema  12121  hashgcdeq  12130  phisum  12131  modprmn0modprm0  12147  pclemub  12178  pclemdc  12179  pcmul  12192  pcqmul  12194  pcdvdstr  12216  ennnfonelemg  12228  ennnfoneleminc  12236  ennnfonelemkh  12237  ennnfonelemhf1o  12238  ennnfonelemex  12239  ennnfonelemhom  12240  ennnfonelemfun  12242  ennnfonelemf1  12243  ennnfonelemrn  12244  ennnfonelemdm  12245  ennnfonelemnn0  12247  ennnfonelemim  12249  exmidunben  12251  ctinfomlemom  12252  ctinf  12255  ctiunctlemudc  12262  nnmindc  12273  nninfdclemlt  12278  nninfdclemf1  12279  isstruct2r  12297  tgdom  12568  neipsm  12650  tgrest  12665  cnfval  12690  cnpfval  12691  cnpval  12694  iscnp4  12714  cnpnei  12715  cnptopco  12718  cncnpi  12724  cncnp  12726  cnptopresti  12734  cnptoprest2  12736  cndis  12737  lmtopcnp  12746  txbasval  12763  neitx  12764  txcnp  12767  txcnmpt  12769  txcn  12771  imasnopn  12795  psmetres2  12829  isxmet2d  12844  xblss2ps  12900  xblss2  12901  blbas  12929  neibl  12987  metss2lem  12993  metrest  13002  xmettx  13006  metcnp3  13007  metcnp  13008  metcnp2  13009  metcnpi  13011  metcnpi2  13012  mulc1cncf  13072  cncfco  13074  mulcncflem  13086  mulcncf  13087  dedekindeulemuub  13091  dedekindeulemloc  13093  dedekindeulemlu  13095  dedekindeu  13097  suplociccreex  13098  suplociccex  13099  dedekindicclemuub  13100  dedekindicclemloc  13102  dedekindicclemlu  13104  dedekindicclemicc  13106  dedekindicc  13107  ivthinclemlopn  13110  ivthinclemlr  13111  ivthinclemuopn  13112  ivthinclemur  13113  ivthinclemloc  13115  ivthinc  13117  limcimolemlt  13129  limccnp2lem  13141  limccnp2cntop  13142  limccoap  13143  dvcj  13169  dveflem  13183  efltlemlt  13191  sin0pilem1  13198  sin0pilem2  13199  pilem3  13200  coseq0negpitopi  13253  abssinper  13263  cos02pilt1  13268  relogeftb  13282  logbgcd1irraplemexp  13382  logbgcd1irrap  13384  bj-findis  13651  pwle2  13667  pwf1oexmid  13668  pw1nct  13672  nnsf  13674  peano4nninf  13675  nninfall  13678  nninfsellemeq  13683  nninfsellemeqinf  13685  qdencn  13695  refeq  13696  trilpolemeq1  13708  trilpolemlt1  13709  trirec0  13712  nconstwlpolemgt0  13731  nconstwlpolem  13732  neapmkvlem  13734