Theorem ad2antrr 479

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 468	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  483  ad5ant13  510  ad5ant23  513  simpll  518  simplll  522  simpllr  523  vtoclgft  2731  reupick  3355  euotd  4171  frirrg  4267  ralxfrd  4378  nnsucpred  4525  foun  5379  f1oprg  5404  dffo4  5561  foeqcnvco  5684  fliftfun  5690  isotr  5710  riotass2  5749  ovmpodxf  5889  mpoxopoveq  6130  tfrlem1  6198  tfrlemibacc  6216  tfrlemibfn  6218  tfrlemi14d  6223  tfrexlem  6224  tfr1onlembacc  6232  tfr1onlembfn  6234  tfr1onlemres  6239  tfrcllembacc  6245  tfrcllembfn  6247  tfrcllemres  6252  frecabcl  6289  nnmordi  6405  eroprf  6515  f1imaen2g  6680  xpen  6732  mapen  6733  mapdom1g  6734  mapxpen  6735  xpmapenlem  6736  phplem4dom  6749  nndomo  6751  phpm  6752  fidifsnen  6757  dif1enen  6767  fisbth  6770  fimax2gtrilemstep  6787  fimax2gtri  6788  en2eqpr  6794  unsnfidcex  6801  unsnfidcel  6802  ssfirab  6815  fidcenumlemrks  6834  sbthlemi8  6845  fiuni  6859  ordiso2  6913  updjud  6960  difinfsnlem  6977  ctssdclemn0  6988  ctssdccl  6989  ctssdc  6991  enumctlemm  6992  enumct  6993  enomnilem  7003  fodju0  7012  exmidfodomrlemim  7050  dfplpq2  7155  nqpi  7179  nqnq0pi  7239  nq0nn  7243  elinp  7275  elnp1st2nd  7277  genprndl  7322  genprndu  7323  addnqprllem  7328  addnqprulem  7329  addnqprl  7330  addnqpru  7331  addlocpr  7337  nqprloc  7346  prmuloc  7367  mulnqprl  7369  mulnqpru  7370  mullocpr  7372  distrlem1prl  7383  distrlem1pru  7384  ltsopr  7397  ltexprlemopl  7402  ltexprlemopu  7404  ltexprlemloc  7408  ltexprlemrl  7411  ltexprlemru  7413  addcanprleml  7415  addcanprlemu  7416  recexprlemloc  7432  recexprlem1ssl  7434  recexprlem1ssu  7435  aptiprleml  7440  aptiprlemu  7441  archpr  7444  cauappcvgprlemm  7446  cauappcvgprlemopl  7447  cauappcvgprlemlol  7448  cauappcvgprlemladdfu  7455  cauappcvgprlemladdfl  7456  cauappcvgprlemladdru  7457  archrecpr  7465  caucvgprlemnkj  7467  caucvgprlemm  7469  caucvgprlemopl  7470  caucvgprlemlol  7471  caucvgprlemdisj  7475  caucvgprlemloc  7476  caucvgprlemladdfu  7478  caucvgprprlemnkltj  7490  caucvgprprlemnkeqj  7491  caucvgprprlemnjltk  7492  caucvgprprlemml  7495  caucvgprprlemopl  7498  caucvgprprlemlol  7499  caucvgprprlemdisj  7503  caucvgprprlemexbt  7507  caucvgprprlemexb  7508  caucvgprprlemaddq  7509  suplocexprlemru  7520  suplocexprlemloc  7522  suplocexprlemex  7523  suplocexprlemub  7524  suplocexprlemlub  7525  mulgt0sr  7579  caucvgsrlemcau  7594  caucvgsrlemoffcau  7599  caucvgsrlemoffres  7601  suplocsrlemb  7607  suplocsrlempr  7608  suplocsrlem  7609  axcaucvglemcau  7699  axcaucvglemres  7700  axpre-suploclemres  7702  axsuploc  7830  cnegexlem1  7930  cnegex  7933  apsym  8361  apcotr  8362  apadd1  8363  mulext1  8367  mulge0  8374  apti  8377  aprcl  8401  conjmulap  8482  lemulge11  8617  creui  8711  nndiv  8754  zaddcllemneg  9086  suprzclex  9142  eluzuzle  9327  divfnzn  9406  qapne  9424  xrltso  9575  xrre  9596  xrre3  9598  xaddf  9620  xaddval  9621  xpncan  9647  xleadd1a  9649  xltadd1  9652  xleaddadd  9663  ixxss12  9682  elioc2  9712  elico2  9713  elicc2  9714  fzm1  9873  fzneuz  9874  eluzgtdifelfzo  9967  elfzonelfzo  10000  exfzdc  10010  qtri3or  10013  exbtwnzlemstep  10018  exbtwnzlemex  10020  exbtwnz  10021  modqid  10115  modqcyc2  10126  modqmuladd  10132  modqmuladdnn0  10134  modaddmodlo  10154  addmodlteq  10164  frecuzrdgrrn  10174  frec2uzrdg  10175  frecuzrdgsuc  10180  frecuzrdgsuctlem  10189  seq3clss  10233  iseqf1olemqcl  10252  iseqf1olemnab  10254  iseqf1olemab  10255  iseqf1olemmo  10258  iseqf1olemqf1o  10259  iseqf1olemjpcl  10261  iseqf1olemqpcl  10262  seq3f1olemqsumk  10265  seq3f1olemqsum  10266  seq3f1olemp  10268  seq3f1oleml  10269  seq3f1o  10270  seq3id3  10273  ser3ge0  10283  exp3val  10288  expap0  10316  facndiv  10478  faclbnd  10480  bcval5  10502  hashunlem  10543  hashun  10544  hashprg  10547  fiprsshashgt1  10556  hashfacen  10572  zfz1isolemiso  10575  zfz1isolem1  10576  seq3coll  10578  ovshftex  10584  2shfti  10596  seq3shft  10603  cjap  10671  caucvgrelemcau  10745  cvg1nlemcau  10749  cvg1nlemres  10750  recvguniq  10760  resqrexlemdecn  10777  resqrexlemcalc3  10781  resqrexlemcvg  10784  resqrexlemoverl  10786  leabs  10839  absexpzap  10845  ltabs  10852  abslt  10853  absle  10854  maxleim  10970  maxabslemval  10973  fimaxre2  10991  minmax  10994  xrmaxiflemcl  11007  xrmaxifle  11008  xrmaxiflemab  11009  xrmaxiflemlub  11010  xrmaxiflemcom  11011  xrmaxltsup  11020  xrmaxadd  11023  xrminmax  11027  xrbdtri  11038  2clim  11063  climshftlemg  11064  climsqz  11097  climsqz2  11098  climrecvg1n  11110  climcvg1nlem  11111  serf0  11114  sumrbdclem  11138  fsum3cvg  11139  summodclem3  11142  summodclem2a  11143  summodclem2  11144  zsumdc  11146  fsum3  11149  isumss  11153  fisumss  11154  fsum3cvg3  11158  fsumcl2lem  11160  fsumadd  11168  fsumsplit  11169  sumsnf  11171  fsum2d  11197  fisum0diag2  11209  fsummulc2  11210  modfsummod  11220  fsumabs  11227  fsumrelem  11233  fsumiun  11239  geoisumr  11280  cvgratnnlemseq  11288  cvgratz  11294  mertenslemi1  11297  mertenslem2  11298  mertensabs  11299  prodrbdclem  11333  fproddccvg  11334  efcj  11368  efaddlem  11369  tanaddaplem  11434  nndivides  11489  dvdsext  11542  divalglemeunn  11607  divalglemex  11608  divalglemeuneg  11609  zsupcllemstep  11627  infssuzex  11631  dvdsbnd  11634  bezoutlemnewy  11673  bezoutlemstep  11674  bezoutlemmain  11675  bezoutlemzz  11679  bezoutlemaz  11680  bezoutlembz  11681  bezoutlemeu  11684  bezoutlemle  11685  bezoutlemsup  11686  dfgcd3  11687  dfgcd2  11691  bezoutr1  11710  dvdslcm  11739  lcmgcdlem  11747  qredeq  11766  qredeu  11767  divgcdcoprm0  11771  divgcdcoprmex  11772  cncongr1  11773  isprm2lem  11786  prmind2  11790  exprmfct  11807  prmdvdsfz  11808  prmexpb  11818  rpexp1i  11821  sqrt2irr  11829  sqne2sq  11844  nonsq  11874  phiprmpw  11887  hashgcdeq  11893  ennnfonelemg  11905  ennnfoneleminc  11913  ennnfonelemkh  11914  ennnfonelemhf1o  11915  ennnfonelemex  11916  ennnfonelemhom  11917  ennnfonelemfun  11919  ennnfonelemf1  11920  ennnfonelemrn  11921  ennnfonelemdm  11922  ennnfonelemnn0  11924  ennnfonelemim  11926  exmidunben  11928  ctinfomlemom  11929  ctinf  11932  ctiunctlemudc  11939  isstruct2r  11959  tgdom  12230  neipsm  12312  tgrest  12327  cnfval  12352  cnpfval  12353  cnpval  12356  iscnp4  12376  cnpnei  12377  cnptopco  12380  cncnpi  12386  cncnp  12388  cnptopresti  12396  cnptoprest2  12398  cndis  12399  lmtopcnp  12408  txbasval  12425  neitx  12426  txcnp  12429  txcnmpt  12431  txcn  12433  imasnopn  12457  psmetres2  12491  isxmet2d  12506  xblss2ps  12562  xblss2  12563  blbas  12591  neibl  12649  metss2lem  12655  metrest  12664  xmettx  12668  metcnp3  12669  metcnp  12670  metcnp2  12671  metcnpi  12673  metcnpi2  12674  mulc1cncf  12734  cncfco  12736  mulcncflem  12748  mulcncf  12749  dedekindeulemuub  12753  dedekindeulemloc  12755  dedekindeulemlu  12757  dedekindeu  12759  suplociccreex  12760  suplociccex  12761  dedekindicclemuub  12762  dedekindicclemloc  12764  dedekindicclemlu  12766  dedekindicclemicc  12768  dedekindicc  12769  ivthinclemlopn  12772  ivthinclemlr  12773  ivthinclemuopn  12774  ivthinclemur  12775  ivthinclemloc  12777  ivthinc  12779  limcimolemlt  12791  limccnp2lem  12803  limccnp2cntop  12804  limccoap  12805  dvcj  12831  dveflem  12844  sin0pilem1  12851  sin0pilem2  12852  pilem3  12853  coseq0negpitopi  12906  abssinper  12916  cos02pilt1  12921  bj-findis  13166  pwle2  13182  pwf1oexmid  13183  nnsf  13188  peano4nninf  13189  nninfalllemn  13191  nninfall  13193  nninfsellemeq  13199  nninfsellemeqinf  13201  qdencn  13211  refeq  13212  trilpolemeq1  13222  trilpolemlt1  13223