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  4673  en2lp  4701  foun  5658  f1oprg  5685  fcof1o  5995  foeqcnvco  5996  f1eqcocnv  5997  caovord3  6263  f1o2ndf1  6464  suppfnss  6497  suppssdc  6500  suppssfvg  6503  smores2  6565  frecrdg  6679  nnaordex  6801  xpdom2  7129  xpen  7145  mapen  7146  xpmapenlem  7149  nndomo  7165  phpm  7167  fidifsnen  7172  isinfinf  7201  fidcen  7203  finexdc  7207  elssdc  7209  fientri3  7222  fiintim  7238  xpfi  7239  f1dmvrnfibi  7258  sbthlemi8  7281  2omap  7319  2omapfi  7321  djudom  7434  omp1eomlem  7435  difinfsn  7441  ctmlemr  7449  ctssdccl  7452  nnnninfeq  7469  enomnilem  7479  finomni  7481  ismkvnex  7496  enmkvlem  7502  nninfwlpoimlemginf  7517  exmidfodomrlemrALT  7556  exmidontriim  7582  netap  7621  exmidapne  7627  acnccim  7639  dfplpq2  7722  recclnq  7760  subhalfnqq  7782  distrnq0  7827  prarloclem3step  7864  genpml  7885  genpmu  7886  addnqprl  7897  addnqpru  7898  appdivnq  7931  mulnqprl  7936  mulnqpru  7937  mullocpr  7939  ltexprlemfl  7977  ltexprlemfu  7979  ltmprr  8010  archpr  8011  cauappcvgprlemm  8013  caucvgprlemladdrl  8046  caucvgprprlemopl  8065  caucvgprprlemopu  8067  recexgt0sr  8141  mulgt0sr  8146  elrealeu  8197  axcaucvglemcau  8266  axcaucvglemres  8267  cnegex  8506  apirr  8936  mulge0  8950  lemul12a  9195  lediv2a  9228  creur  9292  nndiv  9348  zaddcllemneg  9688  peano5uzti  9759  supinfneg  10005  infsupneg  10006  divfnzn  10031  xrltso  10209  xpncan  10284  xltadd1  10289  xleaddadd  10300  elioc2  10349  elico2  10350  elicc2  10351  exfzdc  10670  zsupcllemstep  10673  infssuzex  10677  suprzubdc  10682  exbtwnzlemex  10695  rebtwn2z  10700  modqid  10800  modqcyc  10810  mulqaddmodid  10815  modqadd2mod  10825  addmodlteq  10849  frecuzrdgg  10867  nninfinf  10894  seq3val  10911  seqvalcd  10912  seq3clss  10922  iseqf1olemqcl  10950  iseqf1olemnab  10952  seq3f1olemp  10966  seq3f1o  10968  seqf1oglem1  10970  seqfeq4g  10982  fser0const  10986  ser3ge0  10987  exp3vallem  10991  qsqeqor  11101  nn0sqdc  11161  facndiv  11192  faclbnd  11194  bcval5  11216  hashen  11238  fihashdom  11258  hashunlem  11259  hashfacen  11299  zfz1isolemiso  11306  seq3coll  11309  ccatsymb  11385  ccatrn  11392  ccatw2s1p2  11429  swrdccatin1  11512  swrdccatin2  11516  swrdccat3b  11527  caucvgre  11762  resqrexlemlo  11794  cau3lem  11896  qdenre  11984  rexico  12003  fimaxre2  12009  2zinfmin  12027  xrmaxiflemcl  12029  xrmaxifle  12030  xrmaxiflemcom  12033  2clim  12085  cn1lem  12098  climsqz  12119  climsqz2  12120  climcau  12131  sumrbdclem  12162  summodclem2a  12166  fsum3  12172  fsumcl2lem  12183  fsumadd  12191  sumsnf  12194  fsum2dlemstep  12219  fisum0diag2  12232  fsummulc2  12233  mertenslemub  12319  mertenslemi1  12320  mertensabs  12322  ntrivcvgap  12333  prodrbdclem  12356  prodmodclem3  12360  prodmodclem2a  12361  prodmodc  12363  prod1dc  12371  prodsnf  12377  fprod2dlemstep  12407  efaddlem  12459  tanaddaplem  12523  zdvdsdc  12597  dvdseq  12633  dvdsext  12640  odd2np1  12658  sqoddm1div8z  12671  nno  12691  dfgcd3  12805  nninfctlemfo  12835  dvdslcm  12865  lcmneg  12870  lcmgcdlem  12873  ncoprmgcdne1b  12885  qredeq  12892  qredeu  12893  divgcdcoprm0  12897  exprmfct  12935  prmdvdsfz  12936  isprm5  12939  rpexp1i  12951  sqrt2irr  12959  nonsq  13005  sqrtrirr  13007  eulerthlemrprm  13029  eulerthlema  13030  phisum  13041  modprmn0modprm0  13057  pclemdc  13089  pcz  13133  pcmpt  13144  fldivp1  13149  pcfac  13151  expnprm  13154  oddprmdvds  13155  prmpwdvds  13156  infpnlem1  13160  1arith  13168  4sqlem2  13190  4sqlemafi  13196  4sqleminfi  13198  4sqexercise2  13200  4sqlemsdc  13201  ballotfilemsv  13304  ballotfilemsima  13310  ctinfom  13370  enctlem  13374  nninfdclemlt  13393  setsfun  13438  setsfun0  13439  setscom  13443  gzsumfzval  13762  mndissubm  13833  resmhm  13845  resmhm2  13846  mhmco  13848  gzsumwsubmcl  13852  gzsumwmhm  13854  dfgrp2  13883  isgrpinv  13910  mulgval  13976  mulgnnp1  13984  mulgz  14004  grpissubg  14048  resghm  14114  qusecsub  14186  gsumf1ofi  14211  isrng  14284  lmodfopne  14714  dflidl2rng  14869  mulgrhm2  14996  znidomb  15044  znunit  15045  issubassa2  15086  psrbaglesuppg  15108  psrbagfi  15110  tgdom  15225  ssrest  15335  cnfval  15347  cnpfval  15348  cnpval  15351  iscnp3  15356  ssidcn  15363  cnpnei  15372  cnntr  15378  cncnp  15383  cnptopresti  15391  tx1cn  15422  upxp  15425  imasnopn  15452  bdmet  15655  metcnp  15665  ivthinclemlr  15790  ivthinclemur  15792  ivthinc  15796  dvrecap  15866  dvmptfsum  15878  elply2  15888  plymullem1  15901  plycolemc  15911  plycjlemc  15913  dvply1  15918  pilem3  15937  relogeftb  16019  logbgcd1irr  16125  birthdaylem3  16149  mpodvdsmulf1o  16206  chtublem  16217  mersenne  16219  bposlem1  16233  bposlem3  16235  bposlem5  16237  lgslem4  16244  lgsval  16245  lgsfvalg  16246  lgsval2lem  16251  lgsmod  16267  lgsdir2lem4  16272  lgsdinn0  16289  lgsquad2lem2  16323  lgsquad3  16325  2lgslem1c  16331  2sqlem6  16361  2sqlem7  16362  isupgren  16458  wrdupgren  16459  isumgren  16468  wrdumgren  16469  isuspgren  16520  isusgren  16521  clwwlkext2edg  16785  clwwlknonex2  16802  depindlem3  16871  pw1map  17147  nnsf  17170  peano4nninf  17171  nninfalllem1  17173  nninfsellemqall  17180  nninfsellemeqinf  17181  nninffeq  17185  exmidsbthrlem  17189  isomninnlem  17201  iswomninnlem  17221  iswomni0  17223  ismkvnnlem  17224