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  528  simplrl  535  simplrr  536  ordtri2or2exmidlem  4519  en2lp  4547  foun  5472  f1oprg  5497  fcof1o  5780  foeqcnvco  5781  f1eqcocnv  5782  caovord3  6038  f1o2ndf1  6219  smores2  6285  frecrdg  6399  nnaordex  6519  xpdom2  6821  xpen  6835  mapen  6836  xpmapenlem  6839  nndomo  6854  phpm  6855  fidifsnen  6860  isinfinf  6887  finexdc  6892  fientri3  6904  fiintim  6918  xpfi  6919  f1dmvrnfibi  6933  sbthlemi8  6953  djudom  7082  omp1eomlem  7083  difinfsn  7089  ctmlemr  7097  ctssdccl  7100  nnnninfeq  7116  enomnilem  7126  finomni  7128  ismkvnex  7143  enmkvlem  7149  nninfwlpoimlemginf  7164  exmidfodomrlemrALT  7192  exmidontriim  7214  dfplpq2  7328  recclnq  7366  subhalfnqq  7388  distrnq0  7433  prarloclem3step  7470  genpml  7491  genpmu  7492  addnqprl  7503  addnqpru  7504  appdivnq  7537  mulnqprl  7542  mulnqpru  7543  mullocpr  7545  ltexprlemfl  7583  ltexprlemfu  7585  ltmprr  7616  archpr  7617  cauappcvgprlemm  7619  caucvgprlemladdrl  7652  caucvgprprlemopl  7671  caucvgprprlemopu  7673  recexgt0sr  7747  mulgt0sr  7752  elrealeu  7803  axcaucvglemcau  7872  axcaucvglemres  7873  cnegex  8109  apirr  8536  mulge0  8550  lemul12a  8790  lediv2a  8823  creur  8887  nndiv  8931  zaddcllemneg  9263  peano5uzti  9332  supinfneg  9566  infsupneg  9567  divfnzn  9592  xrltso  9765  xpncan  9840  xltadd1  9845  xleaddadd  9856  elioc2  9905  elico2  9906  elicc2  9907  exfzdc  10208  exbtwnzlemex  10218  rebtwn2z  10223  modqid  10317  modqcyc  10327  mulqaddmodid  10332  modqadd2mod  10342  addmodlteq  10366  frecuzrdgg  10384  seq3val  10426  seqvalcd  10427  seq3clss  10435  iseqf1olemqcl  10454  iseqf1olemnab  10456  seq3f1olemp  10470  seq3f1o  10472  fser0const  10484  ser3ge0  10485  exp3vallem  10489  qsqeqor  10598  facndiv  10685  faclbnd  10687  bcval5  10709  hashen  10730  fihashdom  10749  hashunlem  10750  hashfacen  10782  zfz1isolemiso  10785  seq3coll  10788  caucvgre  10956  resqrexlemlo  10988  cau3lem  11089  qdenre  11177  rexico  11196  fimaxre2  11201  2zinfmin  11217  xrmaxiflemcl  11219  xrmaxifle  11220  xrmaxiflemcom  11223  2clim  11275  cn1lem  11288  climsqz  11309  climsqz2  11310  climcau  11321  sumrbdclem  11351  summodclem2a  11355  fsum3  11361  fsumcl2lem  11372  fsumadd  11380  sumsnf  11383  fsum2dlemstep  11408  fisum0diag2  11421  fsummulc2  11422  mertenslemub  11508  mertenslemi1  11509  mertensabs  11511  ntrivcvgap  11522  prodrbdclem  11545  prodmodclem3  11549  prodmodclem2a  11550  prodmodc  11552  prod1dc  11560  prodsnf  11566  fprod2dlemstep  11596  efaddlem  11648  tanaddaplem  11712  zdvdsdc  11785  dvdseq  11819  dvdsext  11826  odd2np1  11843  sqoddm1div8z  11856  nno  11876  zsupcllemstep  11911  infssuzex  11915  suprzubdc  11918  dfgcd3  11976  dvdslcm  12034  lcmneg  12039  lcmgcdlem  12042  ncoprmgcdne1b  12054  qredeq  12061  qredeu  12062  divgcdcoprm0  12066  exprmfct  12103  prmdvdsfz  12104  isprm5  12107  rpexp1i  12119  sqrt2irr  12127  nonsq  12172  eulerthlemrprm  12194  eulerthlema  12195  phisum  12205  modprmn0modprm0  12221  pclemdc  12253  pcz  12296  pcmpt  12306  fldivp1  12311  pcfac  12313  expnprm  12316  oddprmdvds  12317  prmpwdvds  12318  infpnlem1  12322  1arith  12330  4sqlem2  12352  ctinfom  12394  enctlem  12398  nninfdclemlt  12417  setsfun  12462  setsfun0  12463  setscom  12467  mndissubm  12726  mhmco  12734  dfgrp2  12762  isgrpinv  12786  mulgval  12845  mulgnnp1  12850  mulgz  12869  tgdom  13123  ssrest  13233  cnfval  13245  cnpfval  13246  cnpval  13249  iscnp3  13254  ssidcn  13261  cnpnei  13270  cnntr  13276  cncnp  13281  cnptopresti  13289  tx1cn  13320  upxp  13323  imasnopn  13350  bdmet  13553  metcnp  13563  ivthinclemlr  13666  ivthinclemur  13668  ivthinc  13672  dvrecap  13728  pilem3  13755  relogeftb  13837  logbgcd1irr  13936  lgslem4  13955  lgsval  13956  lgsfvalg  13957  lgsval2lem  13962  lgsmod  13978  lgsdir2lem4  13983  lgsdinn0  14000  2sqlem6  14007  2sqlem7  14008  nnsf  14295  peano4nninf  14296  nninfalllem1  14298  nninfsellemqall  14305  nninfsellemeqinf  14306  nninffeq  14310  exmidsbthrlem  14311  isomninnlem  14319  iswomninnlem  14338  iswomni0  14340  ismkvnnlem  14341