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  4647  en2lp  4675  foun  5632  f1oprg  5659  fcof1o  5961  foeqcnvco  5962  f1eqcocnv  5963  caovord3  6227  f1o2ndf1  6423  suppfnss  6456  suppssdc  6459  suppssfvg  6462  smores2  6524  frecrdg  6638  nnaordex  6760  xpdom2  7081  xpen  7097  mapen  7098  xpmapenlem  7101  nndomo  7117  phpm  7119  fidifsnen  7124  isinfinf  7153  fidcen  7155  finexdc  7159  elssdc  7161  fientri3  7174  fiintim  7190  xpfi  7191  f1dmvrnfibi  7210  sbthlemi8  7233  2omap  7268  2omapfi  7270  djudom  7383  omp1eomlem  7384  difinfsn  7390  ctmlemr  7398  ctssdccl  7401  nnnninfeq  7418  enomnilem  7428  finomni  7430  ismkvnex  7445  enmkvlem  7451  nninfwlpoimlemginf  7466  exmidfodomrlemrALT  7505  exmidontriim  7531  netap  7564  exmidapne  7570  acnccim  7582  dfplpq2  7665  recclnq  7703  subhalfnqq  7725  distrnq0  7770  prarloclem3step  7807  genpml  7828  genpmu  7829  addnqprl  7840  addnqpru  7841  appdivnq  7874  mulnqprl  7879  mulnqpru  7880  mullocpr  7882  ltexprlemfl  7920  ltexprlemfu  7922  ltmprr  7953  archpr  7954  cauappcvgprlemm  7956  caucvgprlemladdrl  7989  caucvgprprlemopl  8008  caucvgprprlemopu  8010  recexgt0sr  8084  mulgt0sr  8089  elrealeu  8140  axcaucvglemcau  8209  axcaucvglemres  8210  cnegex  8447  apirr  8875  mulge0  8889  lemul12a  9132  lediv2a  9165  creur  9229  nndiv  9274  zaddcllemneg  9612  peano5uzti  9682  supinfneg  9923  infsupneg  9924  divfnzn  9949  xrltso  10125  xpncan  10200  xltadd1  10205  xleaddadd  10216  elioc2  10265  elico2  10266  elicc2  10267  exfzdc  10582  zsupcllemstep  10585  infssuzex  10589  suprzubdc  10592  exbtwnzlemex  10605  rebtwn2z  10610  modqid  10707  modqcyc  10717  mulqaddmodid  10722  modqadd2mod  10732  addmodlteq  10756  frecuzrdgg  10774  nninfinf  10801  seq3val  10818  seqvalcd  10819  seq3clss  10829  iseqf1olemqcl  10857  iseqf1olemnab  10859  seq3f1olemp  10873  seq3f1o  10875  seqf1oglem1  10877  seqfeq4g  10889  fser0const  10893  ser3ge0  10894  exp3vallem  10898  qsqeqor  11008  facndiv  11097  faclbnd  11099  bcval5  11121  hashen  11142  fihashdom  11162  hashunlem  11163  hashfacen  11201  zfz1isolemiso  11204  seq3coll  11207  ccatsymb  11283  ccatrn  11290  ccatw2s1p2  11327  swrdccatin1  11410  swrdccatin2  11414  swrdccat3b  11425  caucvgre  11659  resqrexlemlo  11691  cau3lem  11792  qdenre  11880  rexico  11899  fimaxre2  11905  2zinfmin  11921  xrmaxiflemcl  11923  xrmaxifle  11924  xrmaxiflemcom  11927  2clim  11979  cn1lem  11992  climsqz  12013  climsqz2  12014  climcau  12025  sumrbdclem  12056  summodclem2a  12060  fsum3  12066  fsumcl2lem  12077  fsumadd  12085  sumsnf  12088  fsum2dlemstep  12113  fisum0diag2  12126  fsummulc2  12127  mertenslemub  12213  mertenslemi1  12214  mertensabs  12216  ntrivcvgap  12227  prodrbdclem  12250  prodmodclem3  12254  prodmodclem2a  12255  prodmodc  12257  prod1dc  12265  prodsnf  12271  fprod2dlemstep  12301  efaddlem  12353  tanaddaplem  12417  zdvdsdc  12491  dvdseq  12527  dvdsext  12534  odd2np1  12552  sqoddm1div8z  12565  nno  12585  dfgcd3  12699  nninfctlemfo  12729  dvdslcm  12759  lcmneg  12764  lcmgcdlem  12767  ncoprmgcdne1b  12779  qredeq  12786  qredeu  12787  divgcdcoprm0  12791  exprmfct  12828  prmdvdsfz  12829  isprm5  12832  rpexp1i  12844  sqrt2irr  12852  nonsq  12897  eulerthlemrprm  12919  eulerthlema  12920  phisum  12931  modprmn0modprm0  12947  pclemdc  12979  pcz  13023  pcmpt  13034  fldivp1  13039  pcfac  13041  expnprm  13044  oddprmdvds  13045  prmpwdvds  13046  infpnlem1  13050  1arith  13058  4sqlem2  13080  4sqlemafi  13086  4sqleminfi  13088  4sqexercise2  13090  4sqlemsdc  13091  ctinfom  13168  enctlem  13172  nninfdclemlt  13191  setsfun  13236  setsfun0  13237  setscom  13241  gsumfzval  13593  mndissubm  13677  resmhm  13689  resmhm2  13690  mhmco  13692  gsumfzz  13697  gsumwsubmcl  13698  gsumwmhm  13700  dfgrp2  13729  isgrpinv  13756  mulgval  13828  mulgnnp1  13836  mulgz  13856  grpissubg  13900  resghm  13966  qusecsub  14037  isrng  14067  lmodfopne  14461  dflidl2rng  14616  gsumfzfsumlemm  14722  mulgrhm2  14745  znidomb  14793  znunit  14794  psrbaglesuppg  14808  psrbagfi  14810  tgdom  14924  ssrest  15034  cnfval  15046  cnpfval  15047  cnpval  15050  iscnp3  15055  ssidcn  15062  cnpnei  15071  cnntr  15077  cncnp  15082  cnptopresti  15090  tx1cn  15121  upxp  15124  imasnopn  15151  bdmet  15354  metcnp  15364  ivthinclemlr  15489  ivthinclemur  15491  ivthinc  15495  dvrecap  15565  dvmptfsum  15577  elply2  15587  plymullem1  15600  plycolemc  15610  plycjlemc  15612  dvply1  15617  pilem3  15635  relogeftb  15717  logbgcd1irr  15819  mpodvdsmulf1o  15845  mersenne  15852  lgslem4  15863  lgsval  15864  lgsfvalg  15865  lgsval2lem  15870  lgsmod  15886  lgsdir2lem4  15891  lgsdinn0  15908  lgsquad2lem2  15942  lgsquad3  15944  2lgslem1c  15950  2sqlem6  15980  2sqlem7  15981  isupgren  16077  wrdupgren  16078  isumgren  16087  wrdumgren  16088  isuspgren  16139  isusgren  16140  clwwlkext2edg  16404  clwwlknonex2  16421  depindlem3  16490  pw1map  16756  nnsf  16770  peano4nninf  16771  nninfalllem1  16773  nninfsellemqall  16780  nninfsellemeqinf  16781  nninffeq  16785  exmidsbthrlem  16789  isomninnlem  16801  iswomninnlem  16821  iswomni0  16823  ismkvnnlem  16824