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

Theorem ad3antrrr 726
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 481 . 2 ((𝜑𝜒) → 𝜓)
32ad2antrr 722 1 ((((𝜑𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396
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 208  df-an 397
This theorem is referenced by:  ad4antr  728  ad4antlr  729  ad5ant12  752  simplll  771  fsnex  7036  fimaproj  7823  oaabs  8264  oaabs2  8265  omabs  8267  undom  8597  sbthlem8  8626  findcard3  8753  cantnfle  9126  cantnfp1  9136  cantnflem1c  9142  sornom  9691  enfin2i  9735  ttukeylem6  9928  fpwwe2lem13  10056  winalim2  10110  wuncval2  10161  negf1o  11062  xlemul1a  12674  difreicc  12863  flflp1  13170  faclbnd  13643  swrdswrd  14060  pfxccatin12lem3  14087  swrdccat3blem  14094  ello12  14866  elo12  14877  rlimclim1  14895  rlimcld2  14928  o1co  14936  o1of2  14962  o1rlimmul  14968  rlimsqzlem  14998  isercoll  15017  o1fsum  15160  supcvg  15203  dvds2ln  15634  lcmgcdlem  15942  cncongr2  16004  isprm5  16043  pcadd  16217  vdwlem2  16310  vdwlem11  16319  sbcie3s  16533  prdsval  16720  mreexexlem4d  16910  isacs2  16916  catcocl  16948  catass  16949  subccocl  17107  fullsubc  17112  funcco  17133  fullpropd  17182  ffthiso  17191  isnat  17209  natpropd  17238  fucpropd  17239  xpcval  17419  evlf2  17460  curfpropd  17475  curfuncf  17480  uncfcurf  17481  hofcl  17501  hofpropd  17509  yonffthlem  17524  isacs3lem  17768  acsfiindd  17779  gsumpropd2lem  17880  resmhm2b  17972  mhmid  18152  mhmmnd  18153  ghmgrp  18155  conjnmzb  18325  pgpfi  18652  sylow3lem2  18675  efgredlem  18795  frgpnabllem1  18915  dprdfcntz  19059  ablfac1b  19114  pgpfac1lem3  19121  pgpfac1lem5  19123  pgpfaclem3  19127  ringinvnzdiv  19265  cntzsdrg  19503  islmhm2  19732  lspsneleq  19809  psrval  20063  psrass1  20106  resspsrmul  20118  mplbas2  20171  coe1tmmul  20364  gsummoncoe1  20391  znunit  20628  psgndiflemB  20662  uvcff  20853  uvcf1  20854  lindfmm  20889  dmatsubcl  21025  scmatscm  21040  smatvscl  21051  marrepval  21089  mdetdiaglem  21125  mdetunilem8  21146  mdetunilem9  21147  pmatcoe1fsupp  21227  decpmatmulsumfsupp  21299  pmatcollpw2lem  21303  mp2pm2mplem4  21335  pm2mpmhmlem1  21344  pm2mpmhmlem2  21345  pm2mp  21351  fvmptnn04if  21375  cpmadugsumfi  21403  cpmidg2sum  21406  cpmadumatpoly  21409  cayhamlem4  21414  neiptoptop  21657  neitr  21706  ordtrest2lem  21729  cnpnei  21790  iscncl  21795  cncls  21800  cnntr  21801  cncnp  21806  lmcnp  21830  isreg2  21903  hauscmplem  21932  cmpfi  21934  1stcfb  21971  1stcrest  21979  2ndcctbss  21981  2ndcomap  21984  islly2  22010  cldllycmp  22021  lly1stc  22022  locfincmp  22052  llycmpkgen2  22076  1stckgenlem  22079  kgencn2  22083  kgencn3  22084  ptbasfi  22107  ptpjopn  22138  txdis1cn  22161  txlly  22162  txnlly  22163  txtube  22166  txcmplem2  22168  tx1stc  22176  txkgen  22178  xkopt  22181  xkoco2cn  22184  xkococnlem  22185  xkococn  22186  xkoinjcn  22213  tgqtop  22238  regr1lem  22265  kqreglem1  22267  nrmhmph  22320  rnelfmlem  22478  rnelfm  22479  fmfnfmlem4  22483  fmfnfm  22484  ufldom  22488  flimopn  22501  hauspwpwf1  22513  fclsopn  22540  fclsnei  22545  fclsrest  22550  alexsublem  22570  alexsubALTlem3  22575  ptcmplem2  22579  ptcmplem3  22580  cnextfun  22590  cnextcn  22593  symgtgp  22627  tgpt0  22644  qustgpopn  22645  tsmsxplem1  22678  trust  22755  utopsnneiplem  22773  utop3cls  22777  utopreg  22778  isucn2  22805  cstucnd  22810  ucncn  22811  fmucnd  22818  cfilufg  22819  neipcfilu  22822  met2ndci  23049  prdsxmslem2  23056  metustid  23081  metustexhalf  23083  metust  23085  psmetutop  23094  nmoleub  23257  reconnlem2  23352  xrge0tsms  23359  cncfco  23432  lebnumlem3  23484  lebnum  23485  nmoleub2lem2  23637  nmoleub3  23640  iscfil2  23786  iscau4  23799  iscmet3lem2  23812  equivcfil  23819  equivcau  23820  caubl  23828  rrxdstprj1  23929  ovolshftlem2  24028  ovolicc2lem4  24038  uniioombl  24107  i1fmulclem  24220  mbfi1fseqlem6  24238  itg2const2  24259  itg2split  24267  ellimc2  24392  ellimc3  24394  limcflf  24396  dvmptfsum  24489  dvferm1  24499  dvferm2  24501  dvlip2  24509  c1lip1  24511  lhop1  24528  ftc1a  24551  ply1divex  24647  plyeq0lem  24717  plymullem1  24721  coemullem  24757  coemulc  24762  ulmshftlem  24894  ulmcaulem  24899  ulmbdd  24903  ulmcn  24904  ulmdvlem3  24907  mtestbdd  24910  pserulm  24927  pserdvlem2  24933  abelthlem8  24944  xrlimcnp  25462  jensen  25482  lgamucov  25531  logfac2  25709  dchrelbas3  25730  dchrpt  25759  gausslemma2dlem1a  25857  lgsquad3  25879  2sqb  25924  rpvmasumlem  25979  dchrisumlem1  25981  dchrisumlem3  25983  dchrmusum2  25986  dchrvmasumlem2  25990  dchrisum0flblem1  26000  dchrisum0lem1b  26007  dchrisum0lem1  26008  dchrisum0  26012  mulog2sumlem2  26027  pntlem3  26101  ostth3  26130  istrkgcb  26158  tgbtwndiff  26208  iscgrglt  26216  tgcgrxfr  26220  motcgrg  26246  lnext  26269  tgbtwnconn1  26277  tgbtwnconn3  26279  legval  26286  legtrid  26293  legso  26301  hlcgreu  26320  tglnne  26330  tglineeltr  26333  tglnne0  26342  colline  26351  tglowdim2l  26352  tglowdim2ln  26353  mirreu3  26356  mirbtwnhl  26382  krippenlem  26392  midexlem  26394  perpcom  26415  footexALT  26420  footex  26423  colperpexlem3  26434  colperpex  26435  opphllem  26437  midex  26439  oppne3  26445  opptgdim2  26447  oppnid  26448  opphllem2  26450  opphllem5  26453  opphllem6  26454  oppperpex  26455  outpasch  26457  hlpasch  26458  lnopp2hpgb  26465  hpgerlem  26467  colopp  26471  colhp  26472  lmieu  26486  lnperpex  26505  trgcopy  26506  trgcopyeulem  26507  iscgra1  26512  cgrane1  26514  cgrane2  26515  cgrane3  26516  cgrane4  26517  cgrahl1  26518  cgrahl2  26519  cgracgr  26520  cgraswap  26522  cgracom  26524  cgratr  26525  flatcgra  26526  cgrabtwn  26528  cgrahl  26529  sacgr  26533  acopyeu  26536  cgrg3col4  26555  tgasa1  26560  f1otrg  26573  f1otrge  26574  axeuclidlem  26664  axcontlem2  26667  umgrvad2edg  26911  usgredg2vlem2  26924  pthdepisspth  27432  clwwlkccatlem  27683  clwlkclwwlklem2  27694  3cycld  27873  eupth2lems  27933  eucrctshift  27938  frgr3vlem2  27969  n4cyclfrgr  27986  numclwwlk1lem2f1  28052  numclwwlk2lem1  28071  ubthlem3  28565  chirredlem1  30083  chirredlem3  30085  cdj1i  30126  fnpreimac  30333  xrge0infss  30399  nn0xmulclb  30411  hashxpe  30444  ccatf1  30541  swrdf1  30546  xrge0tsmsd  30608  omndmul2  30629  gsumle  30641  psgnfzto1stlem  30658  cycpmco2  30691  cycpmrn  30701  tocyccntz  30702  cycpmconjslem2  30713  cyc3conja  30715  submarchi  30731  suborng  30804  isarchiofld  30806  imaslmod  30838  lindfpropd  30858  qsidomlem1  30871  lindsunlem  30908  lindsun  30909  lbsdiflsp0  30910  dimkerim  30911  fedgmul  30915  extdg1id  30941  smatrcl  30949  1smat1  30957  submateq  30962  mdetpmtr1  30976  madjusmdetlem2  30981  locfinreflem  30992  cmppcmp  31010  ordtrest2NEWlem  31053  ordtconnlem1  31055  lmdvg  31084  esumpcvgval  31225  esum2d  31240  sigapildsys  31309  ldgenpisyslem1  31310  fiunelros  31321  volmeas  31378  imambfm  31408  omssubadd  31446  carsggect  31464  carsgclctunlem3  31466  sgnmul  31688  signsply0  31709  signstres  31733  actfunsnf1o  31763  actfunsnrndisj  31764  reprsuc  31774  reprinfz1  31781  breprexplema  31789  breprexplemc  31791  breprexp  31792  breprexpnat  31793  circlemeth  31799  hgt750lemb  31815  tgoldbachgtd  31821  erdszelem8  32331  pconnconn  32364  cvmlift2lem12  32447  cvmlift3lem5  32456  cvmlift3lem7  32458  cvmlift3lem8  32459  mrsubrn  32646  msrval  32671  msubff1  32689  slerec  33163  btwnconn1lem13  33446  elicc3  33551  neibastop2lem  33594  unbdqndv2  33736  ltflcei  34749  lindsenlbs  34756  matunitlindflem1  34757  matunitlindflem2  34758  poimirlem4  34765  poimirlem13  34774  poimirlem14  34775  poimirlem22  34783  poimirlem26  34787  poimirlem27  34788  heicant  34796  mblfinlem2  34799  mblfinlem3  34800  mblfinlem4  34801  cnambfre  34809  itg2addnclem  34812  itg2addnclem2  34813  itg2gt0cn  34816  bddiblnc  34831  ftc1cnnc  34835  ftc1anclem5  34840  ftc1anclem7  34842  ftc1anc  34844  equivtotbnd  34926  isbndx  34930  ssbnd  34936  heibor1lem  34957  rrncmslem  34980  islshpat  36022  lfl1dim  36126  lfl1dim2N  36127  lkrpssN  36168  glbconN  36382  hlhgt2  36394  3dim2  36473  3dim3  36474  islln3  36515  islvol5  36584  2lplnja  36624  dalem19  36687  isline4N  36782  2polssN  36920  lhpmatb  37036  4atex  37081  trlatn0  37177  cdlemf2  37567  dialss  38051  diaglbN  38060  diaintclN  38063  dibglbN  38171  dibintclN  38172  dihlsscpre  38239  dihglblem5aN  38297  dihglblem2aN  38298  dihglblem4  38302  dihatexv  38343  dihjat1lem  38433  lcfl6  38505  mapdval2N  38635  prjspertr  39122  prjspreln0  39126  elrfi  39158  eldioph2  39226  diophin  39236  irrapxlem2  39287  irrapxlem3  39288  irrapxlem4  39289  irrapxlem5  39290  pell1234qrne0  39317  pell1234qrreccl  39318  pell1234qrmulcl  39319  pell14qrgt0  39323  pell14qrdich  39333  pell1qrge1  39334  pellfundex  39350  congabseq  39438  jm2.27b  39470  jm2.27  39472  fnwe2lem2  39518  kelac1  39530  lnrfg  39586  hbt  39597  rfovcnvf1od  40217  ntrneiiso  40308  ntrneikb  40311  ntrneixb  40312  ntrneik3  40313  ntrneix3  40314  ntrneik13  40315  ntrneix13  40316  cvgdvgrat  40512  binomcxplemnotnn0  40555  sineq0ALT  41138  disjf1  41310  supxrgere  41468  supxrgelem  41472  supxrge  41473  suplesup  41474  xralrple2  41489  infxr  41502  infleinflem2  41506  infleinf  41507  uzub  41572  mccl  41746  limcrecl  41777  lptioo2  41779  lptioo1  41780  lptre2pt  41788  addlimc  41796  limsupmnflem  41868  climxrre  41898  liminflimsupclim  41955  climxlim2lem  41993  xlimliminflimsup  42010  icccncfext  42037  cncfiooicclem1  42043  cncfiooiccre  42045  dvbdfbdioolem2  42081  ioodvbdlimc1lem1  42083  dvnxpaek  42094  dvmptfprodlem  42096  dvmptfprod  42097  dvnprodlem3  42100  itgioocnicc  42129  itgspltprt  42131  stoweidlem31  42184  fourierdlem39  42299  fourierdlem42  42302  fourierdlem48  42307  fourierdlem49  42308  fourierdlem50  42309  fourierdlem51  42310  fourierdlem64  42323  fourierdlem65  42324  fourierdlem74  42333  fourierdlem75  42334  fourierdlem81  42340  fourierdlem82  42341  fourierdlem101  42360  etransclem23  42410  etransclem27  42414  etransclem32  42419  etransclem33  42420  etransclem35  42422  etransclem38  42425  sge0tsms  42530  sge0cl  42531  sge0f1o  42532  sge0split  42559  sge0rpcpnf  42571  sge0seq  42596  nnfoctbdjlem  42605  iundjiun  42610  meaiuninc3v  42634  meaiininclem  42636  omeiunltfirp  42669  carageniuncllem2  42672  carageniuncl  42673  hoidmv1lelem1  42741  hoidmvlelem3  42747  hoidmvlelem5  42749  hoidmvle  42750  hoiqssbllem3  42774  iunhoiioolem  42825  pimdecfgtioo  42863  pimincfltioo  42864  preimageiingt  42866  preimaleiinlt  42867  smflimlem4  42918  iccpartigtl  43417  iccpartgt  43421  sprsymrelf1lem  43487  paireqne  43507  proththd  43613  requad2  43622  sbgoldbst  43777  bgoldbtbndlem4  43807  isomushgr  43825  isomuspgrlem2d  43830  resmgmhm2b  43901  2zrngmmgm  44051  cznrng  44060  rnghmsubcsetclem2  44081  rhmsubcsetclem2  44127  srhmsubc  44181  rhmsubclem4  44194  srhmsubcALTV  44199  rhmsubcALTVlem4  44212  lincsum  44318  lcoss  44325  snlindsntor  44360  islindeps2  44372  line2x  44575  line2y  44576  itscnhlinecirc02p  44606
  Copyright terms: Public domain W3C validator