Theorem ad2antlr 489

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
ad2antlr	⊢ (((𝜒 ∧ 𝜑) ∧ 𝜃) → 𝜓)

Proof of Theorem ad2antlr

Step	Hyp	Ref	Expression
1		ad2ant.1	. . 3 ⊢ (𝜑 → 𝜓)
2	1	adantr 276	. 2 ⊢ ((𝜑 ∧ 𝜃) → 𝜓)
3	2	adantll 476	1 ⊢ (((𝜒 ∧ 𝜑) ∧ 𝜃) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 104

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

This theorem is referenced by:  ad3antlr  493  simplr  529  simplrl  537  simplrr  538  ordtri2or2exmidlem  4653  en2lp  4681  foun  5638  f1oprg  5665  fcof1o  5968  foeqcnvco  5969  f1eqcocnv  5970  caovord3  6236  f1o2ndf1  6437  suppfnss  6470  suppssdc  6473  suppssfvg  6476  smores2  6538  frecrdg  6652  nnaordex  6774  xpdom2  7095  xpen  7111  mapen  7112  xpmapenlem  7115  nndomo  7131  phpm  7133  fidifsnen  7138  isinfinf  7167  fidcen  7169  finexdc  7173  elssdc  7175  fientri3  7188  fiintim  7204  xpfi  7205  f1dmvrnfibi  7224  sbthlemi8  7247  2omap  7282  2omapfi  7284  djudom  7397  omp1eomlem  7398  difinfsn  7404  ctmlemr  7412  ctssdccl  7415  nnnninfeq  7432  enomnilem  7442  finomni  7444  ismkvnex  7459  enmkvlem  7465  nninfwlpoimlemginf  7480  exmidfodomrlemrALT  7519  exmidontriim  7545  netap  7584  exmidapne  7590  acnccim  7602  dfplpq2  7685  recclnq  7723  subhalfnqq  7745  distrnq0  7790  prarloclem3step  7827  genpml  7848  genpmu  7849  addnqprl  7860  addnqpru  7861  appdivnq  7894  mulnqprl  7899  mulnqpru  7900  mullocpr  7902  ltexprlemfl  7940  ltexprlemfu  7942  ltmprr  7973  archpr  7974  cauappcvgprlemm  7976  caucvgprlemladdrl  8009  caucvgprprlemopl  8028  caucvgprprlemopu  8030  recexgt0sr  8104  mulgt0sr  8109  elrealeu  8160  axcaucvglemcau  8229  axcaucvglemres  8230  cnegex  8468  apirr  8897  mulge0  8911  lemul12a  9156  lediv2a  9189  creur  9253  nndiv  9298  zaddcllemneg  9636  peano5uzti  9707  supinfneg  9948  infsupneg  9949  divfnzn  9974  xrltso  10151  xpncan  10226  xltadd1  10231  xleaddadd  10242  elioc2  10291  elico2  10292  elicc2  10293  exfzdc  10611  zsupcllemstep  10614  infssuzex  10618  suprzubdc  10623  exbtwnzlemex  10636  rebtwn2z  10641  modqid  10738  modqcyc  10748  mulqaddmodid  10753  modqadd2mod  10763  addmodlteq  10787  frecuzrdgg  10805  nninfinf  10832  seq3val  10849  seqvalcd  10850  seq3clss  10860  iseqf1olemqcl  10888  iseqf1olemnab  10890  seq3f1olemp  10904  seq3f1o  10906  seqf1oglem1  10908  seqfeq4g  10920  fser0const  10924  ser3ge0  10925  exp3vallem  10929  qsqeqor  11039  facndiv  11129  faclbnd  11131  bcval5  11153  hashen  11175  fihashdom  11195  hashunlem  11196  hashfacen  11236  zfz1isolemiso  11239  seq3coll  11242  ccatsymb  11318  ccatrn  11325  ccatw2s1p2  11362  swrdccatin1  11445  swrdccatin2  11449  swrdccat3b  11460  caucvgre  11694  resqrexlemlo  11726  cau3lem  11827  qdenre  11915  rexico  11934  fimaxre2  11940  2zinfmin  11956  xrmaxiflemcl  11958  xrmaxifle  11959  xrmaxiflemcom  11962  2clim  12014  cn1lem  12027  climsqz  12048  climsqz2  12049  climcau  12060  sumrbdclem  12091  summodclem2a  12095  fsum3  12101  fsumcl2lem  12112  fsumadd  12120  sumsnf  12123  fsum2dlemstep  12148  fisum0diag2  12161  fsummulc2  12162  mertenslemub  12248  mertenslemi1  12249  mertensabs  12251  ntrivcvgap  12262  prodrbdclem  12285  prodmodclem3  12289  prodmodclem2a  12290  prodmodc  12292  prod1dc  12300  prodsnf  12306  fprod2dlemstep  12336  efaddlem  12388  tanaddaplem  12452  zdvdsdc  12526  dvdseq  12562  dvdsext  12569  odd2np1  12587  sqoddm1div8z  12600  nno  12620  dfgcd3  12734  nninfctlemfo  12764  dvdslcm  12794  lcmneg  12799  lcmgcdlem  12802  ncoprmgcdne1b  12814  qredeq  12821  qredeu  12822  divgcdcoprm0  12826  exprmfct  12863  prmdvdsfz  12864  isprm5  12867  rpexp1i  12879  sqrt2irr  12887  nonsq  12932  eulerthlemrprm  12954  eulerthlema  12955  phisum  12966  modprmn0modprm0  12982  pclemdc  13014  pcz  13058  pcmpt  13069  fldivp1  13074  pcfac  13076  expnprm  13079  oddprmdvds  13080  prmpwdvds  13081  infpnlem1  13085  1arith  13093  4sqlem2  13115  4sqlemafi  13121  4sqleminfi  13123  4sqexercise2  13125  4sqlemsdc  13126  ballotfilemsv  13200  ballotfilemsima  13206  ctinfom  13266  enctlem  13270  nninfdclemlt  13289  setsfun  13334  setsfun0  13335  setscom  13339  gsumfzval  13657  mndissubm  13733  resmhm  13745  resmhm2  13746  mhmco  13748  gsumfzz  13753  gsumwsubmcl  13754  gsumwmhm  13756  dfgrp2  13785  isgrpinv  13812  mulgval  13878  mulgnnp1  13886  mulgz  13906  grpissubg  13950  resghm  14016  qusecsub  14087  isrng  14176  lmodfopne  14603  dflidl2rng  14758  gsumfzfsumlemm  14864  mulgrhm2  14887  znidomb  14935  znunit  14936  psrbaglesuppg  14950  psrbagfi  14952  tgdom  15066  ssrest  15176  cnfval  15188  cnpfval  15189  cnpval  15192  iscnp3  15197  ssidcn  15204  cnpnei  15213  cnntr  15219  cncnp  15224  cnptopresti  15232  tx1cn  15263  upxp  15266  imasnopn  15293  bdmet  15496  metcnp  15506  ivthinclemlr  15631  ivthinclemur  15633  ivthinc  15637  dvrecap  15707  dvmptfsum  15719  elply2  15729  plymullem1  15742  plycolemc  15752  plycjlemc  15754  dvply1  15759  pilem3  15777  relogeftb  15859  logbgcd1irr  15961  mpodvdsmulf1o  15987  mersenne  15994  lgslem4  16005  lgsval  16006  lgsfvalg  16007  lgsval2lem  16012  lgsmod  16028  lgsdir2lem4  16033  lgsdinn0  16050  lgsquad2lem2  16084  lgsquad3  16086  2lgslem1c  16092  2sqlem6  16122  2sqlem7  16123  isupgren  16219  wrdupgren  16220  isumgren  16229  wrdumgren  16230  isuspgren  16281  isusgren  16282  clwwlkext2edg  16546  clwwlknonex2  16563  depindlem3  16632  pw1map  16908  nnsf  16922  peano4nninf  16923  nninfalllem1  16925  nninfsellemqall  16932  nninfsellemeqinf  16933  nninffeq  16937  exmidsbthrlem  16941  isomninnlem  16953  iswomninnlem  16973  iswomni0  16975  ismkvnnlem  16976