Theorem ad2antlr 481

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 274	. 2 ⊢ ((𝜑 ∧ 𝜃) → 𝜓)
3	2	adantll 468	1 ⊢ (((𝜒 ∧ 𝜑) ∧ 𝜃) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 103

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

This theorem is referenced by:  ad3antlr  485  simplr  520  simplrl  525  simplrr  526  ordtri2or2exmidlem  4503  en2lp  4531  foun  5451  f1oprg  5476  fcof1o  5757  foeqcnvco  5758  f1eqcocnv  5759  caovord3  6015  f1o2ndf1  6196  smores2  6262  frecrdg  6376  nnaordex  6495  xpdom2  6797  xpen  6811  mapen  6812  xpmapenlem  6815  nndomo  6830  phpm  6831  fidifsnen  6836  isinfinf  6863  finexdc  6868  fientri3  6880  fiintim  6894  xpfi  6895  f1dmvrnfibi  6909  sbthlemi8  6929  djudom  7058  omp1eomlem  7059  difinfsn  7065  ctmlemr  7073  ctssdccl  7076  nnnninfeq  7092  enomnilem  7102  finomni  7104  ismkvnex  7119  enmkvlem  7125  exmidfodomrlemrALT  7159  exmidontriim  7181  dfplpq2  7295  recclnq  7333  subhalfnqq  7355  distrnq0  7400  prarloclem3step  7437  genpml  7458  genpmu  7459  addnqprl  7470  addnqpru  7471  appdivnq  7504  mulnqprl  7509  mulnqpru  7510  mullocpr  7512  ltexprlemfl  7550  ltexprlemfu  7552  ltmprr  7583  archpr  7584  cauappcvgprlemm  7586  caucvgprlemladdrl  7619  caucvgprprlemopl  7638  caucvgprprlemopu  7640  recexgt0sr  7714  mulgt0sr  7719  elrealeu  7770  axcaucvglemcau  7839  axcaucvglemres  7840  cnegex  8076  apirr  8503  mulge0  8517  lemul12a  8757  lediv2a  8790  creur  8854  nndiv  8898  zaddcllemneg  9230  peano5uzti  9299  supinfneg  9533  infsupneg  9534  divfnzn  9559  xrltso  9732  xpncan  9807  xltadd1  9812  xleaddadd  9823  elioc2  9872  elico2  9873  elicc2  9874  exfzdc  10175  exbtwnzlemex  10185  rebtwn2z  10190  modqid  10284  modqcyc  10294  mulqaddmodid  10299  modqadd2mod  10309  addmodlteq  10333  frecuzrdgg  10351  seq3val  10393  seqvalcd  10394  seq3clss  10402  iseqf1olemqcl  10421  iseqf1olemnab  10423  seq3f1olemp  10437  seq3f1o  10439  fser0const  10451  ser3ge0  10452  exp3vallem  10456  qsqeqor  10565  facndiv  10652  faclbnd  10654  bcval5  10676  hashen  10697  fihashdom  10716  hashunlem  10717  hashfacen  10749  zfz1isolemiso  10752  seq3coll  10755  caucvgre  10923  resqrexlemlo  10955  cau3lem  11056  qdenre  11144  rexico  11163  fimaxre2  11168  2zinfmin  11184  xrmaxiflemcl  11186  xrmaxifle  11187  xrmaxiflemcom  11190  2clim  11242  cn1lem  11255  climsqz  11276  climsqz2  11277  climcau  11288  sumrbdclem  11318  summodclem2a  11322  fsum3  11328  fsumcl2lem  11339  fsumadd  11347  sumsnf  11350  fsum2dlemstep  11375  fisum0diag2  11388  fsummulc2  11389  mertenslemub  11475  mertenslemi1  11476  mertensabs  11478  ntrivcvgap  11489  prodrbdclem  11512  prodmodclem3  11516  prodmodclem2a  11517  prodmodc  11519  prod1dc  11527  prodsnf  11533  fprod2dlemstep  11563  efaddlem  11615  tanaddaplem  11679  zdvdsdc  11752  dvdseq  11786  dvdsext  11793  odd2np1  11810  sqoddm1div8z  11823  nno  11843  zsupcllemstep  11878  infssuzex  11882  suprzubdc  11885  dfgcd3  11943  dvdslcm  12001  lcmneg  12006  lcmgcdlem  12009  ncoprmgcdne1b  12021  qredeq  12028  qredeu  12029  divgcdcoprm0  12033  exprmfct  12070  prmdvdsfz  12071  isprm5  12074  rpexp1i  12086  sqrt2irr  12094  nonsq  12139  eulerthlemrprm  12161  eulerthlema  12162  phisum  12172  modprmn0modprm0  12188  pclemdc  12220  pcz  12263  pcmpt  12273  fldivp1  12278  pcfac  12280  expnprm  12283  oddprmdvds  12284  prmpwdvds  12285  infpnlem1  12289  1arith  12297  4sqlem2  12319  ctinfom  12361  enctlem  12365  nninfdclemlt  12384  setsfun  12429  setsfun0  12430  setscom  12434  tgdom  12712  ssrest  12822  cnfval  12834  cnpfval  12835  cnpval  12838  iscnp3  12843  ssidcn  12850  cnpnei  12859  cnntr  12865  cncnp  12870  cnptopresti  12878  tx1cn  12909  upxp  12912  imasnopn  12939  bdmet  13142  metcnp  13152  ivthinclemlr  13255  ivthinclemur  13257  ivthinc  13261  dvrecap  13317  pilem3  13344  relogeftb  13426  logbgcd1irr  13525  lgslem4  13544  lgsval  13545  lgsfvalg  13546  lgsval2lem  13551  lgsmod  13567  lgsdir2lem4  13572  lgsdinn0  13589  2sqlem6  13596  2sqlem7  13597  nnsf  13885  peano4nninf  13886  nninfalllem1  13888  nninfsellemqall  13895  nninfsellemeqinf  13896  nninffeq  13900  exmidsbthrlem  13901  isomninnlem  13909  iswomninnlem  13928  iswomni0  13930  ismkvnnlem  13931