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  4650  en2lp  4678  foun  5635  f1oprg  5662  fcof1o  5964  foeqcnvco  5965  f1eqcocnv  5966  caovord3  6230  f1o2ndf1  6426  suppfnss  6459  suppssdc  6462  suppssfvg  6465  smores2  6527  frecrdg  6641  nnaordex  6763  xpdom2  7084  xpen  7100  mapen  7101  xpmapenlem  7104  nndomo  7120  phpm  7122  fidifsnen  7127  isinfinf  7156  fidcen  7158  finexdc  7162  elssdc  7164  fientri3  7177  fiintim  7193  xpfi  7194  f1dmvrnfibi  7213  sbthlemi8  7236  2omap  7271  2omapfi  7273  djudom  7386  omp1eomlem  7387  difinfsn  7393  ctmlemr  7401  ctssdccl  7404  nnnninfeq  7421  enomnilem  7431  finomni  7433  ismkvnex  7448  enmkvlem  7454  nninfwlpoimlemginf  7469  exmidfodomrlemrALT  7508  exmidontriim  7534  netap  7570  exmidapne  7576  acnccim  7588  dfplpq2  7671  recclnq  7709  subhalfnqq  7731  distrnq0  7776  prarloclem3step  7813  genpml  7834  genpmu  7835  addnqprl  7846  addnqpru  7847  appdivnq  7880  mulnqprl  7885  mulnqpru  7886  mullocpr  7888  ltexprlemfl  7926  ltexprlemfu  7928  ltmprr  7959  archpr  7960  cauappcvgprlemm  7962  caucvgprlemladdrl  7995  caucvgprprlemopl  8014  caucvgprprlemopu  8016  recexgt0sr  8090  mulgt0sr  8095  elrealeu  8146  axcaucvglemcau  8215  axcaucvglemres  8216  cnegex  8453  apirr  8881  mulge0  8895  lemul12a  9138  lediv2a  9171  creur  9235  nndiv  9280  zaddcllemneg  9618  peano5uzti  9689  supinfneg  9930  infsupneg  9931  divfnzn  9956  xrltso  10132  xpncan  10207  xltadd1  10212  xleaddadd  10223  elioc2  10272  elico2  10273  elicc2  10274  exfzdc  10590  zsupcllemstep  10593  infssuzex  10597  suprzubdc  10600  exbtwnzlemex  10613  rebtwn2z  10618  modqid  10715  modqcyc  10725  mulqaddmodid  10730  modqadd2mod  10740  addmodlteq  10764  frecuzrdgg  10782  nninfinf  10809  seq3val  10826  seqvalcd  10827  seq3clss  10837  iseqf1olemqcl  10865  iseqf1olemnab  10867  seq3f1olemp  10881  seq3f1o  10883  seqf1oglem1  10885  seqfeq4g  10897  fser0const  10901  ser3ge0  10902  exp3vallem  10906  qsqeqor  11016  facndiv  11105  faclbnd  11107  bcval5  11129  hashen  11151  fihashdom  11171  hashunlem  11172  hashfacen  11212  zfz1isolemiso  11215  seq3coll  11218  ccatsymb  11294  ccatrn  11301  ccatw2s1p2  11338  swrdccatin1  11421  swrdccatin2  11425  swrdccat3b  11436  caucvgre  11670  resqrexlemlo  11702  cau3lem  11803  qdenre  11891  rexico  11910  fimaxre2  11916  2zinfmin  11932  xrmaxiflemcl  11934  xrmaxifle  11935  xrmaxiflemcom  11938  2clim  11990  cn1lem  12003  climsqz  12024  climsqz2  12025  climcau  12036  sumrbdclem  12067  summodclem2a  12071  fsum3  12077  fsumcl2lem  12088  fsumadd  12096  sumsnf  12099  fsum2dlemstep  12124  fisum0diag2  12137  fsummulc2  12138  mertenslemub  12224  mertenslemi1  12225  mertensabs  12227  ntrivcvgap  12238  prodrbdclem  12261  prodmodclem3  12265  prodmodclem2a  12266  prodmodc  12268  prod1dc  12276  prodsnf  12282  fprod2dlemstep  12312  efaddlem  12364  tanaddaplem  12428  zdvdsdc  12502  dvdseq  12538  dvdsext  12545  odd2np1  12563  sqoddm1div8z  12576  nno  12596  dfgcd3  12710  nninfctlemfo  12740  dvdslcm  12770  lcmneg  12775  lcmgcdlem  12778  ncoprmgcdne1b  12790  qredeq  12797  qredeu  12798  divgcdcoprm0  12802  exprmfct  12839  prmdvdsfz  12840  isprm5  12843  rpexp1i  12855  sqrt2irr  12863  nonsq  12908  eulerthlemrprm  12930  eulerthlema  12931  phisum  12942  modprmn0modprm0  12958  pclemdc  12990  pcz  13034  pcmpt  13045  fldivp1  13050  pcfac  13052  expnprm  13055  oddprmdvds  13056  prmpwdvds  13057  infpnlem1  13061  1arith  13069  4sqlem2  13091  4sqlemafi  13097  4sqleminfi  13099  4sqexercise2  13101  4sqlemsdc  13102  ctinfom  13196  enctlem  13200  nninfdclemlt  13219  setsfun  13264  setsfun0  13265  setscom  13269  gsumfzval  13621  mndissubm  13705  resmhm  13717  resmhm2  13718  mhmco  13720  gsumfzz  13725  gsumwsubmcl  13726  gsumwmhm  13728  dfgrp2  13757  isgrpinv  13784  mulgval  13856  mulgnnp1  13864  mulgz  13884  grpissubg  13928  resghm  13994  qusecsub  14065  isrng  14095  lmodfopne  14491  dflidl2rng  14646  gsumfzfsumlemm  14752  mulgrhm2  14775  znidomb  14823  znunit  14824  psrbaglesuppg  14838  psrbagfi  14840  tgdom  14954  ssrest  15064  cnfval  15076  cnpfval  15077  cnpval  15080  iscnp3  15085  ssidcn  15092  cnpnei  15101  cnntr  15107  cncnp  15112  cnptopresti  15120  tx1cn  15151  upxp  15154  imasnopn  15181  bdmet  15384  metcnp  15394  ivthinclemlr  15519  ivthinclemur  15521  ivthinc  15525  dvrecap  15595  dvmptfsum  15607  elply2  15617  plymullem1  15630  plycolemc  15640  plycjlemc  15642  dvply1  15647  pilem3  15665  relogeftb  15747  logbgcd1irr  15849  mpodvdsmulf1o  15875  mersenne  15882  lgslem4  15893  lgsval  15894  lgsfvalg  15895  lgsval2lem  15900  lgsmod  15916  lgsdir2lem4  15921  lgsdinn0  15938  lgsquad2lem2  15972  lgsquad3  15974  2lgslem1c  15980  2sqlem6  16010  2sqlem7  16011  isupgren  16107  wrdupgren  16108  isumgren  16117  wrdumgren  16118  isuspgren  16169  isusgren  16170  clwwlkext2edg  16434  clwwlknonex2  16451  depindlem3  16520  pw1map  16786  nnsf  16800  peano4nninf  16801  nninfalllem1  16803  nninfsellemqall  16810  nninfsellemeqinf  16811  nninffeq  16815  exmidsbthrlem  16819  isomninnlem  16831  iswomninnlem  16851  iswomni0  16853  ismkvnnlem  16854