Theorem ad2antlr 493

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is used by:  ad3antlr  497  simplr  533  simplrl  541  simplrr  542  ordtri2or2exmidlem  4675  en2lp  4703  foun  5661  f1oprg  5688  fcof1o  5998  foeqcnvco  5999  f1eqcocnv  6000  caovord3  6266  f1o2ndf1  6468  suppfnss  6501  suppssdc  6504  suppssfvg  6507  smores2  6570  frecrdg  6684  nnaordex  6806  xpdom2  7135  xpen  7151  mapen  7152  xpmapenlem  7155  nndomo  7171  phpm  7173  fidifsnen  7178  isinfinf  7207  fidcen  7209  finexdc  7213  elssdc  7215  fientri3  7228  fiintim  7244  xpfi  7245  f1dmvrnfibi  7264  sbthlemi8  7288  2omap  7325  2omapfi  7327  djudom  7440  omp1eomlem  7441  difinfsn  7447  ctmlemr  7455  ctssdccl  7458  nnnninfeq  7475  enomnilem  7485  finomni  7487  ismkvnex  7502  enmkvlem  7508  nninfwlpoimlemginf  7523  exmidfodomrlemrALT  7562  exmidontriim  7588  netap  7627  exmidapne  7633  acnccim  7645  dfplpq2  7728  recclnq  7766  subhalfnqq  7788  distrnq0  7833  prarloclem3step  7870  genpml  7891  genpmu  7892  addnqprl  7903  addnqpru  7904  appdivnq  7937  mulnqprl  7942  mulnqpru  7943  mullocpr  7945  ltexprlemfl  7983  ltexprlemfu  7985  ltmprr  8016  archpr  8017  cauappcvgprlemm  8019  caucvgprlemladdrl  8052  caucvgprprlemopl  8071  caucvgprprlemopu  8073  recexgt0sr  8147  mulgt0sr  8152  elrealeu  8203  axcaucvglemcau  8272  axcaucvglemres  8273  cnegex  8512  apirr  8942  mulge0  8956  lemul12a  9201  lediv2a  9234  creur  9298  nndiv  9355  zaddcllemneg  9693  peano5uzti  9765  supinfneg  10011  infsupneg  10012  divfnzn  10037  xrltso  10215  xpncan  10290  xltadd1  10295  xleaddadd  10306  elioc2  10355  elico2  10356  elicc2  10357  exfzdc  10676  zsupcllemstep  10679  infssuzex  10683  suprzubdc  10688  exbtwnzlemex  10701  rebtwn2z  10706  modqid  10807  modqcyc  10817  mulqaddmodid  10822  modqadd2mod  10832  addmodlteq  10856  frecuzrdgg  10874  nninfinf  10901  seq3val  10918  seqvalcd  10919  seq3clss  10929  iseqf1olemqcl  10957  iseqf1olemnab  10959  seq3f1olemp  10973  seq3f1o  10975  seqf1oglem1  10977  seqfeq4g  10989  fser0const  10993  ser3ge0  10994  exp3vallem  10998  qsqeqor  11108  nn0sqdc  11168  facndiv  11199  faclbnd  11201  bcval5  11223  hashen  11245  fihashdom  11265  hashunlem  11266  hashfacen  11306  zfz1isolemiso  11313  seq3coll  11316  ccatsymb  11392  ccatrn  11399  ccatw2s1p2  11436  swrdccatin1  11519  swrdccatin2  11523  swrdccat3b  11534  caucvgre  11769  resqrexlemlo  11801  cau3lem  11903  qdenre  11991  rexico  12010  fimaxre2  12016  2zinfmin  12034  xrmaxiflemcl  12036  xrmaxifle  12037  xrmaxiflemcom  12040  2clim  12092  cn1lem  12105  climsqz  12126  climsqz2  12127  climcau  12138  sumrbdclem  12169  summodclem2a  12173  fsum3  12179  fsumcl2lem  12190  fsumadd  12198  sumsnf  12201  fsum2dlemstep  12226  fisum0diag2  12239  fsummulc2  12240  mertenslemub  12326  mertenslemi1  12327  mertensabs  12329  ntrivcvgap  12340  prodrbdclem  12363  prodmodclem3  12367  prodmodclem2a  12368  prodmodc  12370  prod1dc  12378  prodsnf  12384  fprod2dlemstep  12414  efaddlem  12466  tanaddaplem  12530  zdvdsdc  12604  dvdseq  12640  dvdsext  12647  odd2np1  12665  sqoddm1div8z  12678  nno  12698  dfgcd3  12812  nninfctlemfo  12842  dvdslcm  12872  lcmneg  12877  lcmgcdlem  12880  ncoprmgcdne1b  12892  qredeq  12899  qredeu  12900  divgcdcoprm0  12904  exprmfct  12942  prmdvdsfz  12943  isprm5  12946  rpexp1i  12958  sqrt2irr  12966  nonsq  13012  sqrtrirr  13014  eulerthlemrprm  13036  eulerthlema  13037  phisum  13048  modprmn0modprm0  13064  pclemdc  13096  pcz  13140  pcmpt  13151  fldivp1  13156  pcfac  13158  expnprm  13161  oddprmdvds  13162  prmpwdvds  13163  infpnlem1  13167  1arith  13175  4sqlem2  13197  4sqlemafi  13203  4sqleminfi  13205  4sqexercise2  13207  4sqlemsdc  13208  ballotfilemsv  13311  ballotfilemsima  13317  ctinfom  13377  enctlem  13381  nninfdclemlt  13400  setsfun  13445  setsfun0  13446  setscom  13450  gzsumfzval  13770  mndissubm  13841  resmhm  13853  resmhm2  13854  mhmco  13856  gzsumwsubmcl  13860  gzsumwmhm  13862  dfgrp2  13891  isgrpinv  13918  mulgval  13984  mulgnnp1  13992  mulgz  14012  grpissubg  14056  resghm  14122  cntzsgrpcl  14167  cntzsubm  14170  cntzmhm  14173  qusecsub  14225  gsumf1ofi  14250  isrng  14340  lmodfopne  14772  dflidl2rng  14927  mulgrhm2  15054  znidomb  15102  znunit  15103  issubassa2  15144  psrbagfi  15167  psrbaglesuppg  15171  tgdom  15331  ssrest  15441  cnfval  15453  cnpfval  15454  cnpval  15457  iscnp3  15462  ssidcn  15469  cnpnei  15478  cnntr  15484  cncnp  15489  cnptopresti  15497  tx1cn  15528  upxp  15531  imasnopn  15558  bdmet  15761  metcnp  15771  ivthinclemlr  15896  ivthinclemur  15898  ivthinc  15902  dvrecap  15972  dvmptfsum  15984  elply2  15994  plymullem1  16007  plycolemc  16017  plycjlemc  16019  dvply1  16024  pilem3  16043  relogeftb  16127  logbgcd1irr  16236  birthdaylem3  16260  mpodvdsmulf1o  16317  chtublem  16328  mersenne  16330  bposlem1  16344  bposlem3  16346  bposlem5  16348  lgslem4  16360  lgsval  16361  lgsfvalg  16362  lgsval2lem  16367  lgsmod  16383  lgsdir2lem4  16388  lgsdinn0  16405  lgsquad2lem2  16439  lgsquad3  16441  2lgslem1c  16447  2sqlem6  16477  2sqlem7  16478  isupgren  16574  wrdupgren  16575  isumgren  16584  wrdumgren  16585  isuspgren  16636  isusgren  16637  clwwlkext2edg  16901  clwwlknonex2  16918  depindlem3  16987  pw1map  17263  nnsf  17287  peano4nninf  17288  nninfalllem1  17290  nninfsellemqall  17297  nninfsellemeqinf  17298  nninffeq  17302  exmidsbthrlem  17306  isomninnlem  17318  iswomninnlem  17339  iswomni0  17341  ismkvnnlem  17342