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  6569  frecrdg  6683  nnaordex  6805  xpdom2  7134  xpen  7150  mapen  7151  xpmapenlem  7154  nndomo  7170  phpm  7172  fidifsnen  7177  isinfinf  7206  fidcen  7208  finexdc  7212  elssdc  7214  fientri3  7227  fiintim  7243  xpfi  7244  f1dmvrnfibi  7263  sbthlemi8  7287  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  9695  peano5uzti  9766  supinfneg  10012  infsupneg  10013  divfnzn  10038  xrltso  10216  xpncan  10291  xltadd1  10296  xleaddadd  10307  elioc2  10356  elico2  10357  elicc2  10358  exfzdc  10677  zsupcllemstep  10680  infssuzex  10684  suprzubdc  10689  exbtwnzlemex  10702  rebtwn2z  10707  modqid  10808  modqcyc  10818  mulqaddmodid  10823  modqadd2mod  10833  addmodlteq  10857  frecuzrdgg  10875  nninfinf  10902  seq3val  10919  seqvalcd  10920  seq3clss  10930  iseqf1olemqcl  10958  iseqf1olemnab  10960  seq3f1olemp  10974  seq3f1o  10976  seqf1oglem1  10978  seqfeq4g  10990  fser0const  10994  ser3ge0  10995  exp3vallem  10999  qsqeqor  11109  nn0sqdc  11169  facndiv  11200  faclbnd  11202  bcval5  11224  hashen  11246  fihashdom  11266  hashunlem  11267  hashfacen  11307  zfz1isolemiso  11314  seq3coll  11317  ccatsymb  11393  ccatrn  11400  ccatw2s1p2  11437  swrdccatin1  11520  swrdccatin2  11524  swrdccat3b  11535  caucvgre  11770  resqrexlemlo  11802  cau3lem  11904  qdenre  11992  rexico  12011  fimaxre2  12017  2zinfmin  12035  xrmaxiflemcl  12037  xrmaxifle  12038  xrmaxiflemcom  12041  2clim  12093  cn1lem  12106  climsqz  12127  climsqz2  12128  climcau  12139  sumrbdclem  12170  summodclem2a  12174  fsum3  12180  fsumcl2lem  12191  fsumadd  12199  sumsnf  12202  fsum2dlemstep  12227  fisum0diag2  12240  fsummulc2  12241  mertenslemub  12327  mertenslemi1  12328  mertensabs  12330  ntrivcvgap  12341  prodrbdclem  12364  prodmodclem3  12368  prodmodclem2a  12369  prodmodc  12371  prod1dc  12379  prodsnf  12385  fprod2dlemstep  12415  efaddlem  12467  tanaddaplem  12531  zdvdsdc  12605  dvdseq  12641  dvdsext  12648  odd2np1  12666  sqoddm1div8z  12679  nno  12699  dfgcd3  12813  nninfctlemfo  12843  dvdslcm  12873  lcmneg  12878  lcmgcdlem  12881  ncoprmgcdne1b  12893  qredeq  12900  qredeu  12901  divgcdcoprm0  12905  exprmfct  12943  prmdvdsfz  12944  isprm5  12947  rpexp1i  12959  sqrt2irr  12967  nonsq  13013  sqrtrirr  13015  eulerthlemrprm  13037  eulerthlema  13038  phisum  13049  modprmn0modprm0  13065  pclemdc  13097  pcz  13141  pcmpt  13152  fldivp1  13157  pcfac  13159  expnprm  13162  oddprmdvds  13163  prmpwdvds  13164  infpnlem1  13168  1arith  13176  4sqlem2  13198  4sqlemafi  13204  4sqleminfi  13206  4sqexercise2  13208  4sqlemsdc  13209  ballotfilemsv  13312  ballotfilemsima  13318  ctinfom  13378  enctlem  13382  nninfdclemlt  13401  setsfun  13446  setsfun0  13447  setscom  13451  gzsumfzval  13771  mndissubm  13842  resmhm  13854  resmhm2  13855  mhmco  13857  gzsumwsubmcl  13861  gzsumwmhm  13863  dfgrp2  13892  isgrpinv  13919  mulgval  13985  mulgnnp1  13993  mulgz  14013  grpissubg  14057  resghm  14123  cntzsgrpcl  14168  cntzsubm  14171  cntzmhm  14174  qusecsub  14226  gsumf1ofi  14251  isrng  14341  lmodfopne  14773  dflidl2rng  14928  mulgrhm2  15055  znidomb  15103  znunit  15104  issubassa2  15145  psrbagfi  15168  psrbaglesuppg  15172  tgdom  15310  ssrest  15420  cnfval  15432  cnpfval  15433  cnpval  15436  iscnp3  15441  ssidcn  15448  cnpnei  15457  cnntr  15463  cncnp  15468  cnptopresti  15476  tx1cn  15507  upxp  15510  imasnopn  15537  bdmet  15740  metcnp  15750  ivthinclemlr  15875  ivthinclemur  15877  ivthinc  15881  dvrecap  15951  dvmptfsum  15963  elply2  15973  plymullem1  15986  plycolemc  15996  plycjlemc  15998  dvply1  16003  pilem3  16022  relogeftb  16106  logbgcd1irr  16215  birthdaylem3  16239  mpodvdsmulf1o  16296  chtublem  16307  mersenne  16309  bposlem1  16323  bposlem3  16325  bposlem5  16327  lgslem4  16339  lgsval  16340  lgsfvalg  16341  lgsval2lem  16346  lgsmod  16362  lgsdir2lem4  16367  lgsdinn0  16384  lgsquad2lem2  16418  lgsquad3  16420  2lgslem1c  16426  2sqlem6  16456  2sqlem7  16457  isupgren  16553  wrdupgren  16554  isumgren  16563  wrdumgren  16564  isuspgren  16615  isusgren  16616  clwwlkext2edg  16880  clwwlknonex2  16897  depindlem3  16966  pw1map  17242  nnsf  17266  peano4nninf  17267  nninfalllem1  17269  nninfsellemqall  17276  nninfsellemeqinf  17277  nninffeq  17281  exmidsbthrlem  17285  isomninnlem  17297  iswomninnlem  17318  iswomni0  17320  ismkvnnlem  17321