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

Theorem ad3antrrr 765
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 761 1 ((((𝜑𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384
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 197  df-an 386
This theorem is referenced by:  ad4antr  767  ad5ant12  1297  fsnex  6503  oaabs  7684  oaabs2  7685  omabs  7687  undom  8008  sbthlem8  8037  findcard3  8163  cantnfle  8528  cantnfp1  8538  cantnflem1c  8544  sornom  9059  enfin2i  9103  ttukeylem6  9296  fpwwe2lem13  9424  fpwwe2  9425  winalim2  9478  wuncval2  9529  negf1o  10420  xlemul1a  12077  difreicc  12262  flflp1  12564  faclbnd  13033  swrdswrd  13414  swrdccatin12lem3  13443  swrdccat3blem  13448  ello12  14197  lo1bdd2  14205  elo12  14208  rlimclim1  14226  rlimcld2  14259  o1co  14267  o1of2  14293  o1rlimmul  14299  rlimsqzlem  14329  isercoll  14348  o1fsum  14491  supcvg  14532  dvds2ln  14957  lcmgcdlem  15262  cncongr2  15325  isprm5  15362  pcadd  15536  vdwlem2  15629  vdwlem11  15638  sbcie3s  15857  prdsval  16055  mreexexlem4d  16247  isacs2  16254  catcocl  16286  catass  16287  subccocl  16445  fullsubc  16450  funcco  16471  funcpropd  16500  fullpropd  16520  ffthiso  16529  isnat  16547  natpropd  16576  fucpropd  16577  xpcval  16757  evlf2  16798  curfpropd  16813  curfuncf  16818  uncfcurf  16819  curf2ndf  16827  hofcl  16839  hofpropd  16847  yonffthlem  16862  isacs3lem  17106  acsfiindd  17117  gsumpropd2lem  17213  resmhm2b  17301  mhmid  17476  mhmmnd  17477  ghmgrp  17479  conjnmzb  17635  pgpfi  17960  sylow3lem2  17983  efgredlem  18100  frgpnabllem1  18216  dprdfcntz  18354  ablfac1b  18409  pgpfac1lem3  18416  pgpfac1lem5  18418  pgpfaclem3  18422  ringinvnzdiv  18533  islmhm2  18978  lspsneleq  19055  psrval  19302  psrass1  19345  resspsrmul  19357  mplbas2  19410  coe1tmmul  19587  gsummoncoe1  19614  znunit  19852  psgndiflemB  19886  uvcff  20070  uvcf1  20071  lindfmm  20106  dmatsubcl  20244  scmatscm  20259  smatvscl  20270  marrepval  20308  mdetdiaglem  20344  mdetunilem8  20365  mdetunilem9  20366  pmatcoe1fsupp  20446  decpmatmulsumfsupp  20518  pmatcollpw2lem  20522  mp2pm2mplem4  20554  pm2mpmhmlem1  20563  pm2mpmhmlem2  20564  pm2mp  20570  fvmptnn04if  20594  cpmadugsumfi  20622  cpmidg2sum  20625  cpmadumatpoly  20628  cayhamlem4  20633  neiptoptop  20875  neitr  20924  ordtrest2lem  20947  cnpnei  21008  iscncl  21013  cncls  21018  cnntr  21019  cncnp  21024  lmcnp  21048  isreg2  21121  hauscmplem  21149  cmpfi  21151  1stcfb  21188  1stcrest  21196  2ndcctbss  21198  2ndcomap  21201  islly2  21227  cldllycmp  21238  lly1stc  21239  locfincmp  21269  llycmpkgen2  21293  1stckgenlem  21296  kgencn2  21300  kgencn3  21301  ptbasfi  21324  ptpjopn  21355  txdis1cn  21378  txlly  21379  txnlly  21380  txtube  21383  txcmplem2  21385  tx1stc  21393  txkgen  21395  xkopt  21398  xkoco2cn  21401  xkococnlem  21402  xkococn  21403  xkoinjcn  21430  tgqtop  21455  regr1lem  21482  kqreglem1  21484  nrmhmph  21537  rnelfmlem  21696  rnelfm  21697  fmfnfmlem4  21701  fmfnfm  21702  ufldom  21706  flimopn  21719  hauspwpwf1  21731  fclsopn  21758  fclsnei  21763  fclsrest  21768  alexsublem  21788  alexsubALTlem3  21793  ptcmplem2  21797  ptcmplem3  21798  cnextfun  21808  cnextcn  21811  symgtgp  21845  tgpt0  21862  qustgpopn  21863  tsmsxplem1  21896  trust  21973  utopsnneiplem  21991  utop3cls  21995  utopreg  21996  isucn2  22023  cstucnd  22028  ucncn  22029  fmucnd  22036  cfilufg  22037  neipcfilu  22040  met2ndci  22267  prdsxmslem2  22274  metcnp3  22285  metustid  22299  metustexhalf  22301  metust  22303  psmetutop  22312  nmoleub  22475  reconnlem2  22570  xrge0tsms  22577  cncfco  22650  lebnumlem3  22702  lebnum  22703  nmoleub2lem2  22856  nmoleub3  22859  iscfil2  23004  iscau4  23017  iscmet3lem2  23030  equivcfil  23037  equivcau  23038  caubl  23046  rrxdstprj1  23132  ovolshftlem2  23218  ovolicc2lem4  23228  uniioombl  23297  i1fmulclem  23409  mbfi1fseqlem6  23427  itg2const2  23448  itg2split  23456  ellimc2  23581  ellimc3  23583  limcflf  23585  dvmptfsum  23676  dvferm1  23686  dvferm2  23688  dvlip2  23696  c1lip1  23698  lhop1  23715  ftc1a  23738  ply1divex  23834  plyeq0lem  23904  plymullem1  23908  coemullem  23944  coemulc  23949  ulmshftlem  24081  ulmcaulem  24086  ulmbdd  24090  ulmcn  24091  ulmdvlem3  24094  mtestbdd  24097  pserulm  24114  pserdvlem2  24120  abelthlem8  24131  xrlimcnp  24629  jensen  24649  lgamucov  24698  logfac2  24876  dchrelbas3  24897  dchrpt  24926  gausslemma2dlem1a  25024  lgsquad3  25046  2sqb  25091  rpvmasumlem  25110  dchrisumlem1  25112  dchrisumlem3  25114  dchrmusum2  25117  dchrvmasumlem2  25121  dchrisum0flblem1  25131  dchrisum0lem1b  25138  dchrisum0lem1  25139  dchrisum0  25143  mulog2sumlem2  25158  pntlem3  25232  ostth3  25261  istrkgcb  25289  tgbtwndiff  25335  iscgrglt  25343  tgcgrxfr  25347  motcgrg  25373  lnext  25396  tgbtwnconn1  25404  tgbtwnconn3  25406  legval  25413  legtrid  25420  legso  25428  hlcgreu  25447  tglnne  25457  tglineeltr  25460  tglnne0  25469  colline  25478  tglowdim2l  25479  tglowdim2ln  25480  mirreu3  25483  mirbtwnhl  25509  krippenlem  25519  midexlem  25521  perpcom  25542  perpneq  25543  footex  25547  colperpexlem3  25558  colperpex  25559  opphllem  25561  midex  25563  oppne3  25569  opptgdim2  25571  oppnid  25572  opphllem2  25574  opphllem5  25577  opphllem6  25578  oppperpex  25579  outpasch  25581  hlpasch  25582  lnopp2hpgb  25589  hpgerlem  25591  colopp  25595  colhp  25596  lmieu  25610  lnperpex  25629  trgcopy  25630  trgcopyeulem  25631  iscgra1  25636  cgrane1  25638  cgrane2  25639  cgrane3  25640  cgrane4  25641  cgrahl1  25642  cgrahl2  25643  cgracgr  25644  cgraswap  25646  cgracom  25648  cgratr  25649  cgrabtwn  25651  cgrahl  25652  sacgr  25656  acopyeu  25659  cgrg3col4  25668  tgasa1  25673  f1otrg  25685  f1otrge  25686  axeuclidlem  25776  axcontlem2  25779  umgrvad2edg  26032  usgredg2vlem2  26045  nbgr2vtx1edg  26167  nbuhgr2vtx1edgb  26169  pthdepisspth  26534  wwlksnwwlksnon  26713  clwlkclwwlklem2  26802  wwlksext2clwwlk  26824  clwlksf1clwwlk  26869  3cycld  26938  eupth2lems  26998  eucrctshift  27003  frgr3vlem2  27036  n4cyclfrgr  27053  numclwwlk2lem1  27124  ubthlem3  27616  chirredlem1  29137  chirredlem3  29139  cdj1i  29180  xrge0infss  29410  omndmul2  29539  submarchi  29567  gsumle  29606  xrge0tsmsd  29612  suborng  29642  isarchiofld  29644  psgnfzto1stlem  29677  fzto1st1  29679  smatrcl  29686  1smat1  29694  submateq  29699  mdetpmtr1  29713  madjusmdetlem2  29718  fimaproj  29724  locfinreflem  29731  cmppcmp  29749  ordtrest2NEWlem  29792  ordtconnlem1  29794  lmdvg  29823  esumpcvgval  29963  esum2d  29978  sigapildsys  30048  ldgenpisyslem1  30049  fiunelros  30060  volmeas  30117  imambfm  30147  omssubadd  30185  carsggect  30203  carsgclctunlem3  30205  sgnmul  30427  signsply0  30450  signstres  30474  erdszelem8  30941  pconnconn  30974  cvmlift2lem12  31057  cvmlift3lem5  31066  cvmlift3lem7  31068  cvmlift3lem8  31069  mrsubrn  31171  msrval  31196  msubff1  31214  nodenselem5  31601  btwnconn1lem13  31901  elicc3  32006  neibastop2lem  32050  unbdqndv2  32197  ltflcei  33068  lindsenlbs  33075  matunitlindflem1  33076  matunitlindflem2  33077  poimirlem4  33084  poimirlem13  33093  poimirlem14  33094  poimirlem22  33102  poimirlem26  33106  poimirlem27  33107  heicant  33115  mblfinlem2  33118  mblfinlem3  33119  mblfinlem4  33120  cnambfre  33129  itg2addnclem  33132  itg2addnclem2  33133  itg2gt0cn  33136  bddiblnc  33151  ftc1cnnc  33155  ftc1anclem5  33160  ftc1anclem7  33162  ftc1anc  33164  equivtotbnd  33248  isbndx  33252  ssbnd  33258  heibor1lem  33279  rrncmslem  33302  islshpat  33823  lfl1dim  33927  lfl1dim2N  33928  lkrpssN  33969  glbconN  34182  hlhgt2  34194  3dim2  34273  3dim3  34274  islln3  34315  islvol5  34384  2lplnja  34424  dalem19  34487  isline4N  34582  2polssN  34720  lhpmatb  34836  4atex  34881  trlatn0  34978  cdlemf2  35369  dialss  35854  diaglbN  35863  diaintclN  35866  dibglbN  35974  dibintclN  35975  dihlsscpre  36042  dihglblem5aN  36100  dihglblem2aN  36101  dihglblem4  36105  dihatexv  36146  dihjat1lem  36236  lcfl6  36308  mapdval2N  36438  elrfi  36776  eldioph2  36844  diophin  36855  irrapxlem2  36906  irrapxlem3  36907  irrapxlem4  36908  irrapxlem5  36909  pell1234qrne0  36936  pell1234qrreccl  36937  pell1234qrmulcl  36938  pell14qrgt0  36942  pell14qrdich  36952  pell1qrge1  36953  pellfundex  36969  congabseq  37060  jm2.27b  37092  jm2.27  37094  fnwe2lem2  37140  kelac1  37152  lnrfg  37209  hbt  37220  cntzsdrg  37292  rfovcnvf1od  37819  ntrneiiso  37910  ntrneikb  37913  ntrneixb  37914  ntrneik3  37915  ntrneix3  37916  ntrneik13  37917  ntrneix13  37918  cvgdvgrat  38033  binomcxplemnotnn0  38076  sineq0ALT  38695  disjf1  38878  supxrgere  39048  supxrgelem  39052  supxrge  39053  suplesup  39054  xralrple2  39069  infxr  39082  infleinflem2  39086  infleinf  39087  uzub  39157  mccl  39266  limcrecl  39297  lptioo2  39299  lptioo1  39300  lptre2pt  39308  addlimc  39316  limsupmnflem  39388  icccncfext  39435  cncfiooicclem1  39441  cncfiooiccre  39443  dvbdfbdioolem2  39481  ioodvbdlimc1lem1  39483  dvnxpaek  39494  dvmptfprodlem  39496  dvmptfprod  39497  dvnprodlem3  39500  itgioocnicc  39530  itgspltprt  39532  stoweidlem31  39585  fourierdlem39  39700  fourierdlem42  39703  fourierdlem48  39708  fourierdlem49  39709  fourierdlem50  39710  fourierdlem51  39711  fourierdlem64  39724  fourierdlem65  39725  fourierdlem74  39734  fourierdlem75  39735  fourierdlem81  39741  fourierdlem82  39742  fourierdlem101  39761  etransclem23  39811  etransclem27  39815  etransclem32  39820  etransclem33  39821  etransclem35  39823  etransclem38  39826  sge0tsms  39934  sge0cl  39935  sge0f1o  39936  sge0split  39963  sge0rpcpnf  39975  sge0seq  40000  nnfoctbdjlem  40009  iundjiun  40014  meaiininclem  40037  omeiunltfirp  40070  carageniuncllem2  40073  carageniuncl  40074  hoidmv1lelem1  40142  hoidmvlelem3  40148  hoidmvlelem5  40150  hoidmvle  40151  hoiqssbllem3  40175  iunhoiioolem  40226  pimdecfgtioo  40264  pimincfltioo  40265  preimageiingt  40267  preimaleiinlt  40268  smflimlem4  40319  iccpartigtl  40687  iccpartgt  40691  proththd  40860  bgoldbst  40991  bgoldbtbndlem4  41015  sprsymrelf1lem  41059  resmgmhm2b  41118  2zrngmmgm  41264  cznrng  41273  rnghmsubcsetclem2  41294  rhmsubcsetclem2  41340  srhmsubc  41394  rhmsubclem4  41407  srhmsubcALTV  41412  rhmsubcALTVlem4  41425  lincsum  41536  lcoss  41543  snlindsntor  41578  islindeps2  41590
  Copyright terms: Public domain W3C validator