MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ad3antrrr Structured version   Visualization version   GIF version

Theorem ad3antrrr 761
Description: Deduction adding three conjuncts to antecedent. (Contributed by NM, 28-Jul-2012.)
Hypothesis
Ref Expression
ad2ant.1 (𝜑𝜓)
Assertion
Ref Expression
ad3antrrr ((((𝜑𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜓)

Proof of Theorem ad3antrrr
StepHypRef Expression
1 ad2ant.1 . . 3 (𝜑𝜓)
21adantr 479 . 2 ((𝜑𝜒) → 𝜓)
32ad2antrr 757 1 ((((𝜑𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 195  df-an 384
This theorem is referenced by:  ad4antr  763  ad5ant12  1291  fsnex  6413  oaabs  7585  oaabs2  7586  omabs  7588  undom  7907  sbthlem8  7936  findcard3  8062  cantnfle  8425  cantnfp1  8435  cantnflem1c  8441  sornom  8956  enfin2i  9000  ttukeylem6  9193  fpwwe2lem13  9317  fpwwe2  9318  winalim2  9371  wuncval2  9422  negf1o  10308  xlemul1a  11944  difreicc  12128  flflp1  12422  faclbnd  12891  swrdswrd  13255  swrdccatin12lem3  13284  swrdccat3blem  13289  ello12  14038  lo1bdd2  14046  elo12  14049  rlimclim1  14067  rlimcld2  14100  o1co  14108  o1of2  14134  o1rlimmul  14140  rlimsqzlem  14170  isercoll  14189  o1fsum  14329  supcvg  14370  dvds2ln  14795  lcmgcdlem  15100  cncongr2  15163  isprm5  15200  pcadd  15374  vdwlem2  15467  vdwlem11  15476  sbcie3s  15688  prdsval  15881  mreexexlem4d  16073  isacs2  16080  catcocl  16112  catass  16113  subccocl  16271  fullsubc  16276  funcco  16297  funcpropd  16326  fullpropd  16346  ffthiso  16355  isnat  16373  natpropd  16402  fucpropd  16403  xpcval  16583  evlf2  16624  curfpropd  16639  curfuncf  16644  uncfcurf  16645  curf2ndf  16653  hofcl  16665  hofpropd  16673  yonffthlem  16688  isacs3lem  16932  acsfiindd  16943  gsumpropd2lem  17039  resmhm2b  17127  mhmid  17302  mhmmnd  17303  ghmgrp  17305  conjnmzb  17461  pgpfi  17786  sylow3lem2  17809  efgredlem  17926  frgpnabllem1  18042  dprdfcntz  18180  ablfac1b  18235  pgpfac1lem3  18242  pgpfac1lem5  18244  pgpfaclem3  18248  ringinvnzdiv  18359  islmhm2  18802  lspsneleq  18879  psrval  19126  psrass1  19169  resspsrmul  19181  mplbas2  19234  coe1tmmul  19411  gsummoncoe1  19438  znunit  19673  psgndiflemB  19707  uvcff  19888  uvcf1  19889  lindfmm  19924  dmatsubcl  20062  scmatscm  20077  smatvscl  20088  marrepval  20126  mdetdiaglem  20162  mdetunilem8  20183  mdetunilem9  20184  pmatcoe1fsupp  20264  decpmatmulsumfsupp  20336  pmatcollpw2lem  20340  mp2pm2mplem4  20372  pm2mpmhmlem1  20381  pm2mpmhmlem2  20382  pm2mp  20388  fvmptnn04if  20412  cpmadugsumfi  20440  cpmidg2sum  20443  cpmadumatpoly  20446  cayhamlem4  20451  neiptoptop  20684  neitr  20733  ordtrest2lem  20756  cnpnei  20817  iscncl  20822  cncls  20827  cnntr  20828  cncnp  20833  lmcnp  20857  isreg2  20930  hauscmplem  20958  cmpfi  20960  1stcfb  20997  1stcrest  21005  2ndcctbss  21007  2ndcomap  21010  islly2  21036  cldllycmp  21047  lly1stc  21048  locfincmp  21078  llycmpkgen2  21102  1stckgenlem  21105  kgencn2  21109  kgencn3  21110  ptbasfi  21133  ptpjopn  21164  txdis1cn  21187  txlly  21188  txnlly  21189  txtube  21192  txcmplem2  21194  tx1stc  21202  txkgen  21204  xkopt  21207  xkoco2cn  21210  xkococnlem  21211  xkococn  21212  xkoinjcn  21239  tgqtop  21264  regr1lem  21291  kqreglem1  21293  nrmhmph  21346  rnelfmlem  21505  rnelfm  21506  fmfnfmlem4  21510  fmfnfm  21511  ufldom  21515  flimopn  21528  hauspwpwf1  21540  fclsopn  21567  fclsnei  21572  fclsrest  21577  alexsublem  21597  alexsubALTlem3  21602  ptcmplem2  21606  ptcmplem3  21607  cnextfun  21617  cnextcn  21620  symgtgp  21654  tgpt0  21671  qustgpopn  21672  tsmsxplem1  21705  trust  21782  utopsnneiplem  21800  utop3cls  21804  utopreg  21805  isucn2  21832  cstucnd  21837  ucncn  21838  fmucnd  21845  cfilufg  21846  neipcfilu  21849  met2ndci  22075  prdsxmslem2  22082  metcnp3  22093  metustid  22107  metustexhalf  22109  metust  22111  psmetutop  22120  nmoleub  22274  reconnlem2  22367  xrge0tsms  22374  cncfco  22446  lebnumlem3  22498  lebnum  22499  nmoleub2lem2  22652  nmoleub3  22655  iscfil2  22787  iscau4  22800  iscmet3lem2  22813  equivcfil  22820  equivcau  22821  caubl  22828  rrxdstprj1  22914  ovolshftlem2  22999  ovolicc2lem4  23009  uniioombl  23077  i1fmulclem  23189  mbfi1fseqlem6  23207  itg2const2  23228  itg2split  23236  ellimc2  23361  ellimc3  23363  limcflf  23365  dvmptfsum  23456  dvferm1  23466  dvferm2  23468  dvlip2  23476  c1lip1  23478  lhop1  23495  ftc1a  23518  ply1divex  23614  plyeq0lem  23684  plymullem1  23688  coemullem  23724  coemulc  23729  ulmshftlem  23861  ulmcaulem  23866  ulmbdd  23870  ulmcn  23871  ulmdvlem3  23874  mtestbdd  23877  pserulm  23894  pserdvlem2  23900  abelthlem8  23911  xrlimcnp  24409  jensen  24429  lgamucov  24478  logfac2  24656  dchrelbas3  24677  dchrpt  24706  gausslemma2dlem1a  24804  lgsquad3  24826  2sqb  24871  rpvmasumlem  24890  dchrisumlem1  24892  dchrisumlem3  24894  dchrmusum2  24897  dchrvmasumlem2  24901  dchrisum0flblem1  24911  dchrisum0lem1b  24918  dchrisum0lem1  24919  dchrisum0  24923  mulog2sumlem2  24938  pntlem3  25012  ostth3  25041  istrkgcb  25069  tgbtwndiff  25115  iscgrglt  25124  tgcgrxfr  25128  motcgrg  25154  lnext  25177  tgbtwnconn1  25185  tgbtwnconn3  25187  legval  25194  legtrid  25201  legso  25209  hlcgreu  25228  tglnne  25238  tglineeltr  25241  tglnne0  25250  colline  25259  tglowdim2l  25260  tglowdim2ln  25261  mirreu3  25264  mirbtwnhl  25290  krippenlem  25300  midexlem  25302  perpcom  25323  perpneq  25324  footex  25328  colperpexlem3  25339  colperpex  25340  opphllem  25342  midex  25344  oppne3  25350  opptgdim2  25352  oppnid  25353  opphllem2  25355  opphllem5  25358  opphllem6  25359  oppperpex  25360  outpasch  25362  hlpasch  25363  lnopp2hpgb  25370  hpgerlem  25372  colopp  25376  colhp  25377  lmieu  25391  lnperpex  25410  trgcopy  25411  trgcopyeulem  25412  iscgra1  25417  cgrane1  25419  cgrane2  25420  cgrane3  25421  cgrane4  25422  cgrahl1  25423  cgrahl2  25424  cgracgr  25425  cgraswap  25427  cgracom  25429  cgratr  25430  cgrabtwn  25432  cgrahl  25433  sacgr  25437  acopyeu  25440  cgrg3col4  25449  tgasa1  25454  f1otrg  25466  f1otrge  25467  axeuclidlem  25557  axcontlem2  25560  usgraidx2vlem2  25684  usgrares1  25702  nbgraf1olem5  25737  usgra2wlkspth  25912  constr3cycl  25952  clwlkisclwwlklem1  26078  wwlkext2clwwlk  26094  eupath2  26270  frisusgranb  26287  frgra2v  26289  frgra3vlem2  26291  2pthfrgrarn2  26300  2spotiundisj  26352  usg2spot2nb  26355  usgreghash2spotv  26356  numclwwlk2lem1  26392  ubthlem3  26915  chirredlem1  28436  chirredlem3  28438  cdj1i  28479  xrge0infss  28718  omndmul2  28846  submarchi  28874  gsumle  28913  xrge0tsmsd  28919  suborng  28949  isarchiofld  28951  psgnfzto1stlem  28984  fzto1st1  28986  smatrcl  28993  1smat1  29001  submateq  29006  mdetpmtr1  29020  madjusmdetlem2  29025  fimaproj  29031  locfinreflem  29038  cmppcmp  29056  ordtrest2NEWlem  29099  ordtconlem1  29101  lmdvg  29130  esumpcvgval  29270  esum2d  29285  sigapildsys  29355  ldgenpisyslem1  29356  fiunelros  29367  volmeas  29424  imambfm  29454  omssubadd  29492  carsggect  29510  carsgclctunlem3  29512  sgnmul  29734  signsply0  29757  signstres  29781  erdszelem8  30237  pconcon  30270  cvmlift2lem12  30353  cvmlift3lem5  30362  cvmlift3lem7  30364  cvmlift3lem8  30365  mrsubrn  30467  msrval  30492  msubff1  30510  nodenselem5  30887  btwnconn1lem13  31179  elicc3  31284  neibastop2lem  31328  unbdqndv2  31475  ltflcei  32367  lindsenlbs  32374  matunitlindflem1  32375  matunitlindflem2  32376  poimirlem4  32383  poimirlem13  32392  poimirlem14  32393  poimirlem22  32401  poimirlem26  32405  poimirlem27  32406  heicant  32414  mblfinlem2  32417  mblfinlem3  32418  mblfinlem4  32419  cnambfre  32428  itg2addnclem  32431  itg2addnclem2  32432  itg2gt0cn  32435  bddiblnc  32450  ftc1cnnc  32454  ftc1anclem5  32459  ftc1anclem7  32461  ftc1anc  32463  equivtotbnd  32547  isbndx  32551  ssbnd  32557  heibor1lem  32578  rrncmslem  32601  islshpat  33122  lfl1dim  33226  lfl1dim2N  33227  lkrpssN  33268  glbconN  33481  hlhgt2  33493  3dim2  33572  3dim3  33573  islln3  33614  islvol5  33683  2lplnja  33723  dalem19  33786  isline4N  33881  2polssN  34019  lhpmatb  34135  4atex  34180  trlatn0  34277  cdlemf2  34668  dialss  35153  diaglbN  35162  diaintclN  35165  dibglbN  35273  dibintclN  35274  dihlsscpre  35341  dihglblem5aN  35399  dihglblem2aN  35400  dihglblem4  35404  dihatexv  35445  dihjat1lem  35535  lcfl6  35607  mapdval2N  35737  elrfi  36075  eldioph2  36143  diophin  36154  irrapxlem2  36205  irrapxlem3  36206  irrapxlem4  36207  irrapxlem5  36208  pell1234qrne0  36235  pell1234qrreccl  36236  pell1234qrmulcl  36237  pell14qrgt0  36241  pell14qrdich  36251  pell1qrge1  36252  pellfundex  36268  congabseq  36359  jm2.27b  36391  jm2.27  36393  fnwe2lem2  36439  kelac1  36451  lnrfg  36508  hbt  36519  cntzsdrg  36591  rfovcnvf1od  37118  ntrneiiso  37209  ntrneikb  37212  ntrneixb  37213  ntrneik3  37214  ntrneix3  37215  ntrneik13  37216  ntrneix13  37217  cvgdvgrat  37334  binomcxplemnotnn0  37377  sineq0ALT  37995  disjf1  38164  supxrgere  38291  supxrgelem  38295  supxrge  38296  suplesup  38297  xralrple2  38312  infxr  38325  infleinflem2  38329  infleinf  38330  mccl  38466  limcrecl  38497  lptioo2  38499  lptioo1  38500  lptre2pt  38508  addlimc  38516  icccncfext  38574  cncfiooicclem1  38580  cncfiooiccre  38582  dvbdfbdioolem2  38620  ioodvbdlimc1lem1  38622  dvnxpaek  38633  dvmptfprodlem  38635  dvmptfprod  38636  dvnprodlem3  38639  itgioocnicc  38670  itgspltprt  38672  stoweidlem31  38725  fourierdlem39  38840  fourierdlem42  38843  fourierdlem48  38848  fourierdlem49  38849  fourierdlem50  38850  fourierdlem51  38851  fourierdlem64  38864  fourierdlem65  38865  fourierdlem74  38874  fourierdlem75  38875  fourierdlem81  38881  fourierdlem82  38882  fourierdlem101  38901  etransclem23  38951  etransclem27  38955  etransclem32  38960  etransclem33  38961  etransclem35  38963  etransclem38  38966  sge0tsms  39074  sge0cl  39075  sge0f1o  39076  sge0split  39103  sge0rpcpnf  39115  sge0seq  39140  nnfoctbdjlem  39149  iundjiun  39154  meaiininclem  39177  omeiunltfirp  39210  carageniuncllem2  39213  carageniuncl  39214  hoidmv1lelem1  39282  hoidmvlelem3  39288  hoidmvlelem5  39290  hoidmvle  39291  hoiqssbllem3  39315  iunhoiioolem  39367  pimdecfgtioo  39405  pimincfltioo  39406  preimageiingt  39408  preimaleiinlt  39409  smflimlem4  39461  iccpartigtl  39763  iccpartgt  39767  proththd  39871  bgoldbst  40002  bgoldbtbndlem4  40026  umgrvad2edg  40439  usgredg2vlem2  40452  nbgr2vtx1edg  40571  nbuhgr2vtx1edgb  40573  pthdepissPth  40940  wwlksnwwlksnon  41120  clwlkclwwlklem2  41208  wwlksext2clwwlk  41230  clwlksf1clwwlk  41275  3cycld  41344  eupth2lems  41405  eucrctshift  41410  frgr3vlem2  41443  n4cyclfrgr  41460  av-numclwwlk2lem1  41531  resmgmhm2b  41589  2zrngmmgm  41735  cznrng  41746  rnghmsubcsetclem2  41767  rhmsubcsetclem2  41813  srhmsubc  41867  rhmsubclem4  41880  srhmsubcALTV  41886  rhmsubcALTVlem4  41899  lincsum  42011  lcoss  42018  snlindsntor  42053  islindeps2  42065
  Copyright terms: Public domain W3C validator