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  2736  reupick  3360  euotd  4176  frirrg  4272  ralxfrd  4383  nnsucpred  4530  foun  5386  f1oprg  5411  dffo4  5568  foeqcnvco  5691  fliftfun  5697  isotr  5717  riotass2  5756  ovmpodxf  5896  mpoxopoveq  6137  tfrlem1  6205  tfrlemibacc  6223  tfrlemibfn  6225  tfrlemi14d  6230  tfrexlem  6231  tfr1onlembacc  6239  tfr1onlembfn  6241  tfr1onlemres  6246  tfrcllembacc  6252  tfrcllembfn  6254  tfrcllemres  6259  frecabcl  6296  nnmordi  6412  eroprf  6522  f1imaen2g  6687  xpen  6739  mapen  6740  mapdom1g  6741  mapxpen  6742  xpmapenlem  6743  phplem4dom  6756  nndomo  6758  phpm  6759  fidifsnen  6764  dif1enen  6774  fisbth  6777  fimax2gtrilemstep  6794  fimax2gtri  6795  en2eqpr  6801  unsnfidcex  6808  unsnfidcel  6809  ssfirab  6822  fidcenumlemrks  6841  sbthlemi8  6852  fiuni  6866  ordiso2  6920  updjud  6967  difinfsnlem  6984  ctssdclemn0  6995  ctssdccl  6996  ctssdc  6998  enumctlemm  6999  enumct  7000  enomnilem  7010  fodju0  7019  exmidfodomrlemim  7057  dfplpq2  7162  nqpi  7186  nqnq0pi  7246  nq0nn  7250  elinp  7282  elnp1st2nd  7284  genprndl  7329  genprndu  7330  addnqprllem  7335  addnqprulem  7336  addnqprl  7337  addnqpru  7338  addlocpr  7344  nqprloc  7353  prmuloc  7374  mulnqprl  7376  mulnqpru  7377  mullocpr  7379  distrlem1prl  7390  distrlem1pru  7391  ltsopr  7404  ltexprlemopl  7409  ltexprlemopu  7411  ltexprlemloc  7415  ltexprlemrl  7418  ltexprlemru  7420  addcanprleml  7422  addcanprlemu  7423  recexprlemloc  7439  recexprlem1ssl  7441  recexprlem1ssu  7442  aptiprleml  7447  aptiprlemu  7448  archpr  7451  cauappcvgprlemm  7453  cauappcvgprlemopl  7454  cauappcvgprlemlol  7455  cauappcvgprlemladdfu  7462  cauappcvgprlemladdfl  7463  cauappcvgprlemladdru  7464  archrecpr  7472  caucvgprlemnkj  7474  caucvgprlemm  7476  caucvgprlemopl  7477  caucvgprlemlol  7478  caucvgprlemdisj  7482  caucvgprlemloc  7483  caucvgprlemladdfu  7485  caucvgprprlemnkltj  7497  caucvgprprlemnkeqj  7498  caucvgprprlemnjltk  7499  caucvgprprlemml  7502  caucvgprprlemopl  7505  caucvgprprlemlol  7506  caucvgprprlemdisj  7510  caucvgprprlemexbt  7514  caucvgprprlemexb  7515  caucvgprprlemaddq  7516  suplocexprlemru  7527  suplocexprlemloc  7529  suplocexprlemex  7530  suplocexprlemub  7531  suplocexprlemlub  7532  mulgt0sr  7586  caucvgsrlemcau  7601  caucvgsrlemoffcau  7606  caucvgsrlemoffres  7608  suplocsrlemb  7614  suplocsrlempr  7615  suplocsrlem  7616  axcaucvglemcau  7706  axcaucvglemres  7707  axpre-suploclemres  7709  axsuploc  7837  cnegexlem1  7937  cnegex  7940  apsym  8368  apcotr  8369  apadd1  8370  mulext1  8374  mulge0  8381  apti  8384  aprcl  8408  conjmulap  8489  lemulge11  8624  creui  8718  nndiv  8761  zaddcllemneg  9093  suprzclex  9149  eluzuzle  9334  divfnzn  9413  qapne  9431  xrltso  9582  xrre  9603  xrre3  9605  xaddf  9627  xaddval  9628  xpncan  9654  xleadd1a  9656  xltadd1  9659  xleaddadd  9670  ixxss12  9689  elioc2  9719  elico2  9720  elicc2  9721  fzm1  9880  fzneuz  9881  eluzgtdifelfzo  9974  elfzonelfzo  10007  exfzdc  10017  qtri3or  10020  exbtwnzlemstep  10025  exbtwnzlemex  10027  exbtwnz  10028  modqid  10122  modqcyc2  10133  modqmuladd  10139  modqmuladdnn0  10141  modaddmodlo  10161  addmodlteq  10171  frecuzrdgrrn  10181  frec2uzrdg  10182  frecuzrdgsuc  10187  frecuzrdgsuctlem  10196  seq3clss  10240  iseqf1olemqcl  10259  iseqf1olemnab  10261  iseqf1olemab  10262  iseqf1olemmo  10265  iseqf1olemqf1o  10266  iseqf1olemjpcl  10268  iseqf1olemqpcl  10269  seq3f1olemqsumk  10272  seq3f1olemqsum  10273  seq3f1olemp  10275  seq3f1oleml  10276  seq3f1o  10277  seq3id3  10280  ser3ge0  10290  exp3val  10295  expap0  10323  facndiv  10485  faclbnd  10487  bcval5  10509  hashunlem  10550  hashun  10551  hashprg  10554  fiprsshashgt1  10563  hashfacen  10579  zfz1isolemiso  10582  zfz1isolem1  10583  seq3coll  10585  ovshftex  10591  2shfti  10603  seq3shft  10610  cjap  10678  caucvgrelemcau  10752  cvg1nlemcau  10756  cvg1nlemres  10757  recvguniq  10767  resqrexlemdecn  10784  resqrexlemcalc3  10788  resqrexlemcvg  10791  resqrexlemoverl  10793  leabs  10846  absexpzap  10852  ltabs  10859  abslt  10860  absle  10861  maxleim  10977  maxabslemval  10980  fimaxre2  10998  minmax  11001  xrmaxiflemcl  11014  xrmaxifle  11015  xrmaxiflemab  11016  xrmaxiflemlub  11017  xrmaxiflemcom  11018  xrmaxltsup  11027  xrmaxadd  11030  xrminmax  11034  xrbdtri  11045  2clim  11070  climshftlemg  11071  climsqz  11104  climsqz2  11105  climrecvg1n  11117  climcvg1nlem  11118  serf0  11121  sumrbdclem  11146  fsum3cvg  11147  summodclem3  11149  summodclem2a  11150  summodclem2  11151  zsumdc  11153  fsum3  11156  isumss  11160  fisumss  11161  fsum3cvg3  11165  fsumcl2lem  11167  fsumadd  11175  fsumsplit  11176  sumsnf  11178  fsum2d  11204  fisum0diag2  11216  fsummulc2  11217  modfsummod  11227  fsumabs  11234  fsumrelem  11240  fsumiun  11246  geoisumr  11287  cvgratnnlemseq  11295  cvgratz  11301  mertenslemi1  11304  mertenslem2  11305  mertensabs  11306  prodrbdclem  11340  fproddccvg  11341  prodmodclem3  11344  prodmodclem2a  11345  efcj  11379  efaddlem  11380  tanaddaplem  11445  nndivides  11500  dvdsext  11553  divalglemeunn  11618  divalglemex  11619  divalglemeuneg  11620  zsupcllemstep  11638  infssuzex  11642  dvdsbnd  11645  bezoutlemnewy  11684  bezoutlemstep  11685  bezoutlemmain  11686  bezoutlemzz  11690  bezoutlemaz  11691  bezoutlembz  11692  bezoutlemeu  11695  bezoutlemle  11696  bezoutlemsup  11697  dfgcd3  11698  dfgcd2  11702  bezoutr1  11721  dvdslcm  11750  lcmgcdlem  11758  qredeq  11777  qredeu  11778  divgcdcoprm0  11782  divgcdcoprmex  11783  cncongr1  11784  isprm2lem  11797  prmind2  11801  exprmfct  11818  prmdvdsfz  11819  prmexpb  11829  rpexp1i  11832  sqrt2irr  11840  sqne2sq  11855  nonsq  11885  phiprmpw  11898  hashgcdeq  11904  ennnfonelemg  11916  ennnfoneleminc  11924  ennnfonelemkh  11925  ennnfonelemhf1o  11926  ennnfonelemex  11927  ennnfonelemhom  11928  ennnfonelemfun  11930  ennnfonelemf1  11931  ennnfonelemrn  11932  ennnfonelemdm  11933  ennnfonelemnn0  11935  ennnfonelemim  11937  exmidunben  11939  ctinfomlemom  11940  ctinf  11943  ctiunctlemudc  11950  isstruct2r  11970  tgdom  12241  neipsm  12323  tgrest  12338  cnfval  12363  cnpfval  12364  cnpval  12367  iscnp4  12387  cnpnei  12388  cnptopco  12391  cncnpi  12397  cncnp  12399  cnptopresti  12407  cnptoprest2  12409  cndis  12410  lmtopcnp  12419  txbasval  12436  neitx  12437  txcnp  12440  txcnmpt  12442  txcn  12444  imasnopn  12468  psmetres2  12502  isxmet2d  12517  xblss2ps  12573  xblss2  12574  blbas  12602  neibl  12660  metss2lem  12666  metrest  12675  xmettx  12679  metcnp3  12680  metcnp  12681  metcnp2  12682  metcnpi  12684  metcnpi2  12685  mulc1cncf  12745  cncfco  12747  mulcncflem  12759  mulcncf  12760  dedekindeulemuub  12764  dedekindeulemloc  12766  dedekindeulemlu  12768  dedekindeu  12770  suplociccreex  12771  suplociccex  12772  dedekindicclemuub  12773  dedekindicclemloc  12775  dedekindicclemlu  12777  dedekindicclemicc  12779  dedekindicc  12780  ivthinclemlopn  12783  ivthinclemlr  12784  ivthinclemuopn  12785  ivthinclemur  12786  ivthinclemloc  12788  ivthinc  12790  limcimolemlt  12802  limccnp2lem  12814  limccnp2cntop  12815  limccoap  12816  dvcj  12842  dveflem  12855  sin0pilem1  12862  sin0pilem2  12863  pilem3  12864  coseq0negpitopi  12917  abssinper  12927  cos02pilt1  12932  bj-findis  13177  pwle2  13193  pwf1oexmid  13194  nnsf  13199  peano4nninf  13200  nninfalllemn  13202  nninfall  13204  nninfsellemeq  13210  nninfsellemeqinf  13212  qdencn  13222  refeq  13223  trilpolemeq1  13233  trilpolemlt1  13234