Theorem ad2antrr 471

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

Syntax hints:   → wi 4   ∧ wa 102

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

This theorem is referenced by:  ad3antrrr  475  simpll  495  simplll  499  simpllr  500  vtoclgft  2649  reupick  3248  euotd  4009  frirrg  4105  ralxfrd  4212  foun  5165  f1oprg  5188  dffo4  5336  foeqcnvco  5450  fliftfun  5456  isotr  5476  riotass2  5514  ovmpt2dxf  5646  mpt2xopoveq  5878  tfrlem1  5946  tfrlemibacc  5963  tfrlemibfn  5965  tfrlemi14d  5970  tfrexlem  5971  nnmordi  6112  eroprf  6222  f1imaen2g  6296  phplem4dom  6348  nndomo  6350  phpm  6351  fidifsnen  6355  fisbth  6367  en2eqpr  6380  unsnfidcex  6385  unsnfidcel  6386  ordiso2  6446  dfplpq2  6544  nqpi  6568  nqnq0pi  6628  nq0nn  6632  elinp  6664  elnp1st2nd  6666  genprndl  6711  genprndu  6712  addnqprllem  6717  addnqprulem  6718  addnqprl  6719  addnqpru  6720  addlocpr  6726  nqprloc  6735  prmuloc  6756  mulnqprl  6758  mulnqpru  6759  mullocpr  6761  distrlem1prl  6772  distrlem1pru  6773  ltsopr  6786  ltexprlemopl  6791  ltexprlemopu  6793  ltexprlemloc  6797  ltexprlemrl  6800  ltexprlemru  6802  addcanprleml  6804  addcanprlemu  6805  recexprlemloc  6821  recexprlem1ssl  6823  recexprlem1ssu  6824  aptiprleml  6829  aptiprlemu  6830  archpr  6833  cauappcvgprlemm  6835  cauappcvgprlemopl  6836  cauappcvgprlemlol  6837  cauappcvgprlemladdfu  6844  cauappcvgprlemladdfl  6845  cauappcvgprlemladdru  6846  archrecpr  6854  caucvgprlemnkj  6856  caucvgprlemm  6858  caucvgprlemopl  6859  caucvgprlemlol  6860  caucvgprlemdisj  6864  caucvgprlemloc  6865  caucvgprlemladdfu  6867  caucvgprprlemnkltj  6879  caucvgprprlemnkeqj  6880  caucvgprprlemnjltk  6881  caucvgprprlemml  6884  caucvgprprlemopl  6887  caucvgprprlemlol  6888  caucvgprprlemdisj  6892  caucvgprprlemexbt  6896  caucvgprprlemexb  6897  caucvgprprlemaddq  6898  mulgt0sr  6954  caucvgsrlemcau  6969  caucvgsrlemoffcau  6974  caucvgsrlemoffres  6976  axcaucvglemcau  7064  axcaucvglemres  7065  cnegexlem1  7283  cnegex  7286  apsym  7706  apcotr  7707  apadd1  7708  mulext1  7712  mulge0  7719  apti  7722  conjmulap  7817  lemulge11  7944  creui  8037  nndiv  8079  zaddcllemneg  8390  suprzclex  8445  eluzuzle  8627  divfnzn  8706  qapne  8724  xrltso  8871  xrre  8887  xrre3  8889  ixxss12  8929  elioc2  8959  elico2  8960  elicc2  8961  fzm1  9117  fzneuz  9118  eluzgtdifelfzo  9206  elfzonelfzo  9239  exfzdc  9249  qtri3or  9252  qbtwnzlemstep  9257  qbtwnzlemex  9259  qbtwnz  9260  modqid  9351  modqcyc2  9362  modqmuladd  9368  modqmuladdnn0  9370  modaddmodlo  9390  addmodlteq  9400  frecuzrdgrrn  9410  iseqid3s  9466  expival  9478  expap0  9506  facndiv  9666  faclbnd  9668  ibcval5  9690  ovshftex  9707  2shfti  9719  cjap  9793  caucvgrelemcau  9866  cvg1nlemcau  9870  cvg1nlemres  9871  recvguniq  9881  resqrexlemdecn  9898  resqrexlemcalc3  9902  resqrexlemcvg  9905  resqrexlemoverl  9907  leabs  9960  absexpzap  9966  ltabs  9973  abslt  9974  absle  9975  maxleim  10091  maxabslemval  10094  fimaxre2  10109  minmax  10112  2clim  10140  climshftlemg  10141  climsqz  10173  climsqz2  10174  climrecvg1n  10185  climcvg1nlem  10186  serif0  10189  nndivides  10202  dvdsext  10255  divalglemeunn  10321  divalglemex  10322  divalglemeuneg  10323  zsupcllemstep  10341  infssuzex  10345  dvdsbnd  10348  bezoutlemnewy  10385  bezoutlemstep  10386  bezoutlemmain  10387  bezoutlemzz  10391  bezoutlemaz  10392  bezoutlembz  10393  bezoutlemeu  10396  bezoutlemle  10397  bezoutlemsup  10398  dfgcd3  10399  dfgcd2  10403  bezoutr1  10422  dvdslcm  10451  lcmgcdlem  10459  qredeq  10478  qredeu  10479  divgcdcoprm0  10483  divgcdcoprmex  10484  cncongr1  10485  isprm2lem  10498  prmind2  10502  exprmfct  10519  prmdvdsfz  10520  prmexpb  10530  rpexp1i  10533  sqrt2irr  10541  sqne2sq  10555  bj-findis  10774  qdencn  10785