Theorem ad2antrr 473

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

Syntax hints:   → wi 4   ∧ wa 103

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

This theorem is referenced by:  ad3antrrr  477  simpll  497  simplll  501  simpllr  502  vtoclgft  2683  reupick  3299  euotd  4105  frirrg  4201  ralxfrd  4312  foun  5307  f1oprg  5330  dffo4  5486  foeqcnvco  5607  fliftfun  5613  isotr  5633  riotass2  5672  ovmpt2dxf  5808  mpt2xopoveq  6043  tfrlem1  6111  tfrlemibacc  6129  tfrlemibfn  6131  tfrlemi14d  6136  tfrexlem  6137  tfr1onlembacc  6145  tfr1onlembfn  6147  tfr1onlemres  6152  tfrcllembacc  6158  tfrcllembfn  6160  tfrcllemres  6165  frecabcl  6202  nnmordi  6315  eroprf  6425  f1imaen2g  6590  xpen  6641  mapen  6642  mapdom1g  6643  mapxpen  6644  xpmapenlem  6645  phplem4dom  6658  nndomo  6660  phpm  6661  fidifsnen  6666  dif1enen  6676  fisbth  6679  fimax2gtrilemstep  6696  fimax2gtri  6697  en2eqpr  6703  unsnfidcex  6710  unsnfidcel  6711  ssfirab  6723  fidcenumlemrks  6742  sbthlemi8  6753  ordiso2  6808  updjud  6853  enumctlemm  6872  enumct  6873  enomnilem  6881  fodju0  6890  exmidfodomrlemim  6924  dfplpq2  7010  nqpi  7034  nqnq0pi  7094  nq0nn  7098  elinp  7130  elnp1st2nd  7132  genprndl  7177  genprndu  7178  addnqprllem  7183  addnqprulem  7184  addnqprl  7185  addnqpru  7186  addlocpr  7192  nqprloc  7201  prmuloc  7222  mulnqprl  7224  mulnqpru  7225  mullocpr  7227  distrlem1prl  7238  distrlem1pru  7239  ltsopr  7252  ltexprlemopl  7257  ltexprlemopu  7259  ltexprlemloc  7263  ltexprlemrl  7266  ltexprlemru  7268  addcanprleml  7270  addcanprlemu  7271  recexprlemloc  7287  recexprlem1ssl  7289  recexprlem1ssu  7290  aptiprleml  7295  aptiprlemu  7296  archpr  7299  cauappcvgprlemm  7301  cauappcvgprlemopl  7302  cauappcvgprlemlol  7303  cauappcvgprlemladdfu  7310  cauappcvgprlemladdfl  7311  cauappcvgprlemladdru  7312  archrecpr  7320  caucvgprlemnkj  7322  caucvgprlemm  7324  caucvgprlemopl  7325  caucvgprlemlol  7326  caucvgprlemdisj  7330  caucvgprlemloc  7331  caucvgprlemladdfu  7333  caucvgprprlemnkltj  7345  caucvgprprlemnkeqj  7346  caucvgprprlemnjltk  7347  caucvgprprlemml  7350  caucvgprprlemopl  7353  caucvgprprlemlol  7354  caucvgprprlemdisj  7358  caucvgprprlemexbt  7362  caucvgprprlemexb  7363  caucvgprprlemaddq  7364  mulgt0sr  7420  caucvgsrlemcau  7435  caucvgsrlemoffcau  7440  caucvgsrlemoffres  7442  axcaucvglemcau  7530  axcaucvglemres  7531  cnegexlem1  7754  cnegex  7757  apsym  8180  apcotr  8181  apadd1  8182  mulext1  8186  mulge0  8193  apti  8196  conjmulap  8293  lemulge11  8424  creui  8518  nndiv  8561  zaddcllemneg  8887  suprzclex  8943  eluzuzle  9126  divfnzn  9205  qapne  9223  xrltso  9365  xrre  9386  xrre3  9388  xaddf  9410  xaddval  9411  xpncan  9437  xleadd1a  9439  xltadd1  9442  xleaddadd  9453  ixxss12  9472  elioc2  9502  elico2  9503  elicc2  9504  fzm1  9663  fzneuz  9664  eluzgtdifelfzo  9757  elfzonelfzo  9790  exfzdc  9800  qtri3or  9803  exbtwnzlemstep  9808  exbtwnzlemex  9810  exbtwnz  9811  modqid  9905  modqcyc2  9916  modqmuladd  9922  modqmuladdnn0  9924  modaddmodlo  9944  addmodlteq  9954  frecuzrdgrrn  9964  frec2uzrdg  9965  frecuzrdgsuc  9970  frecuzrdgsuctlem  9979  seq3clss  10032  iseqf1olemqcl  10052  iseqf1olemnab  10054  iseqf1olemab  10055  iseqf1olemmo  10058  iseqf1olemqf1o  10059  iseqf1olemjpcl  10061  iseqf1olemqpcl  10062  seq3f1olemqsumk  10065  seq3f1olemqsum  10066  seq3f1olemp  10068  seq3f1oleml  10069  seq3f1o  10070  seq3id3  10073  ser3ge0  10083  exp3val  10088  expap0  10116  facndiv  10278  faclbnd  10280  bcval5  10302  hashunlem  10343  hashun  10344  hashprg  10347  fiprsshashgt1  10356  hashfacen  10372  zfz1isolemiso  10375  zfz1isolem1  10376  seq3coll  10378  ovshftex  10384  2shfti  10396  seq3shft  10403  cjap  10471  caucvgrelemcau  10544  cvg1nlemcau  10548  cvg1nlemres  10549  recvguniq  10559  resqrexlemdecn  10576  resqrexlemcalc3  10580  resqrexlemcvg  10583  resqrexlemoverl  10585  leabs  10638  absexpzap  10644  ltabs  10651  abslt  10652  absle  10653  maxleim  10769  maxabslemval  10772  fimaxre2  10789  minmax  10792  xrmaxiflemcl  10804  xrmaxifle  10805  xrmaxiflemab  10806  xrmaxiflemlub  10807  xrmaxiflemcom  10808  xrmaxltsup  10817  xrmaxadd  10820  xrminmax  10824  xrbdtri  10835  2clim  10860  climshftlemg  10861  climsqz  10894  climsqz2  10895  climrecvg1n  10907  climcvg1nlem  10908  serf0  10911  sumrbdclem  10935  fsum3cvg  10936  summodclem3  10939  summodclem2a  10940  summodclem2  10941  zsumdc  10943  fsum3  10946  isumss  10950  fisumss  10951  fsum3cvg3  10955  fsumcl2lem  10957  fsumadd  10965  fsumsplit  10966  sumsnf  10968  fsum2d  10994  fisum0diag2  11006  fsummulc2  11007  modfsummod  11017  fsumabs  11024  fsumrelem  11030  fsumiun  11036  geoisumr  11077  cvgratnnlemseq  11085  cvgratz  11091  mertenslemi1  11094  mertenslem2  11095  mertensabs  11096  efcj  11128  efaddlem  11129  tanaddaplem  11194  nndivides  11246  dvdsext  11299  divalglemeunn  11364  divalglemex  11365  divalglemeuneg  11366  zsupcllemstep  11384  infssuzex  11388  dvdsbnd  11391  bezoutlemnewy  11428  bezoutlemstep  11429  bezoutlemmain  11430  bezoutlemzz  11434  bezoutlemaz  11435  bezoutlembz  11436  bezoutlemeu  11439  bezoutlemle  11440  bezoutlemsup  11441  dfgcd3  11442  dfgcd2  11446  bezoutr1  11465  dvdslcm  11494  lcmgcdlem  11502  qredeq  11521  qredeu  11522  divgcdcoprm0  11526  divgcdcoprmex  11527  cncongr1  11528  isprm2lem  11541  prmind2  11545  exprmfct  11562  prmdvdsfz  11563  prmexpb  11573  rpexp1i  11576  sqrt2irr  11584  sqne2sq  11598  nonsq  11628  phiprmpw  11641  hashgcdeq  11647  isstruct2r  11670  tgdom  11940  neipsm  12022  tgrest  12037  cnfval  12062  cnpfval  12063  cnpval  12065  iscnp4  12085  cnpnei  12086  cnptopco  12089  cncnpi  12095  cncnp  12097  cnptopresti  12105  cnptoprest2  12107  cndis  12108  lmtopcnp  12117  psmetres2  12135  isxmet2d  12150  xblss2ps  12206  xblss2  12207  blbas  12235  neibl  12293  metss2lem  12299  metrest  12308  metcnp3  12309  metcnp  12310  metcnp2  12311  metcnpi  12313  metcnpi2  12314  mulc1cncf  12358  cncfco  12360  mulcncflem  12369  mulcncf  12370  bj-findis  12598  nnsucpred  12612  nnsf  12616  peano4nninf  12617  nninfalllemn  12619  nninfall  12621  nninfsellemeq  12627  nninfsellemeqinf  12629  qdencn  12636