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

Theorem ad3antrrr 729
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 482 . 2 ((𝜑𝜒) → 𝜓)
32ad2antrr 725 1 ((((𝜑𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397
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 206  df-an 398
This theorem is referenced by:  ad4antr  731  ad4antlr  732  ad5ant12  755  simplll  774  fsnex  7230  fimaproj  8068  frxp3  8084  oaabs  8595  oaabs2  8596  omabs  8598  cofon1  8619  undomOLD  9005  sbthlem8  9035  findcard3OLD  9231  cantnfle  9608  cantnfp1  9618  cantnflem1c  9624  sornom  10214  enfin2i  10258  ttukeylem6  10451  fpwwe2lem12  10579  winalim2  10633  wuncval2  10684  negf1o  11586  xlemul1a  13208  difreicc  13402  flflp1  13713  faclbnd  14191  swrdswrd  14594  pfxccatin12lem3  14621  swrdccat3blem  14628  ello12  15399  elo12  15410  rlimclim1  15428  rlimcld2  15461  o1co  15469  o1of2  15496  o1rlimmul  15502  rlimsqzlem  15534  isercoll  15553  o1fsum  15699  supcvg  15742  dvds2ln  16172  lcmgcdlem  16483  cncongr2  16545  isprm5  16584  prmdvdsncoprmbd  16603  pcadd  16762  vdwlem2  16855  vdwlem11  16864  sbcie3s  17035  prdsval  17338  mreexexlem4d  17528  isacs2  17534  catcocl  17566  catass  17567  subccocl  17732  fullsubc  17737  funcco  17758  fullpropd  17808  ffthiso  17817  isnat  17835  natpropd  17866  fucpropd  17867  xpcval  18066  evlf2  18108  curfpropd  18123  curfuncf  18128  uncfcurf  18129  hofcl  18149  hofpropd  18157  yonffthlem  18172  isacs3lem  18432  acsfiindd  18443  gsumpropd2lem  18535  resmhm2b  18634  mhmid  18869  mhmmnd  18870  ghmgrp  18872  conjnmzb  19044  pgpfi  19388  sylow3lem2  19411  efgredlem  19530  frgpnabllem1  19652  dprdfcntz  19795  ablfac1b  19850  pgpfac1lem3  19857  pgpfac1lem5  19859  pgpfaclem3  19863  ringinvnzdiv  20018  cntzsdrg  20272  islmhm2  20502  lspsneleq  20579  znunit  20973  psgndiflemB  21007  uvcff  21200  uvcf1  21201  lindfmm  21236  psrval  21320  psrass1  21377  resspsrmul  21389  mplbas2  21446  mhpmulcl  21542  coe1tmmul  21651  gsummoncoe1  21678  dmatsubcl  21850  scmatscm  21865  smatvscl  21876  marrepval  21914  mdetdiaglem  21950  mdetunilem8  21971  mdetunilem9  21972  pmatcoe1fsupp  22053  decpmatmulsumfsupp  22125  pmatcollpw2lem  22129  mp2pm2mplem4  22161  pm2mpmhmlem1  22170  pm2mpmhmlem2  22171  pm2mp  22177  fvmptnn04if  22201  cpmadugsumfi  22229  cpmidg2sum  22232  cpmadumatpoly  22235  cayhamlem4  22240  neiptoptop  22485  neitr  22534  ordtrest2lem  22557  cnpnei  22618  iscncl  22623  cncls  22628  cnntr  22629  cncnp  22634  lmcnp  22658  isreg2  22731  hauscmplem  22760  cmpfi  22762  1stcfb  22799  1stcrest  22807  2ndcctbss  22809  2ndcomap  22812  islly2  22838  cldllycmp  22849  lly1stc  22850  locfincmp  22880  llycmpkgen2  22904  1stckgenlem  22907  kgencn2  22911  kgencn3  22912  ptbasfi  22935  ptpjopn  22966  txdis1cn  22989  txlly  22990  txnlly  22991  txtube  22994  txcmplem2  22996  tx1stc  23004  txkgen  23006  xkopt  23009  xkoco2cn  23012  xkococnlem  23013  xkococn  23014  xkoinjcn  23041  tgqtop  23066  regr1lem  23093  kqreglem1  23095  nrmhmph  23148  rnelfmlem  23306  rnelfm  23307  fmfnfmlem4  23311  fmfnfm  23312  ufldom  23316  flimopn  23329  hauspwpwf1  23341  fclsopn  23368  fclsnei  23373  fclsrest  23378  alexsublem  23398  alexsubALTlem3  23403  ptcmplem2  23407  ptcmplem3  23408  cnextfun  23418  cnextcn  23421  symgtgp  23460  tgpt0  23473  qustgpopn  23474  tsmsxplem1  23507  trust  23584  utopsnneiplem  23602  utop3cls  23606  utopreg  23607  isucn2  23634  cstucnd  23639  ucncn  23640  fmucnd  23647  cfilufg  23648  neipcfilu  23651  met2ndci  23881  prdsxmslem2  23888  metustid  23913  metustexhalf  23915  metust  23917  psmetutop  23926  nmoleub  24098  reconnlem2  24193  xrge0tsms  24200  cncfco  24273  lebnumlem3  24329  lebnum  24330  nmoleub2lem2  24482  nmoleub3  24485  iscfil2  24633  iscau4  24646  iscmet3lem2  24659  equivcfil  24666  equivcau  24667  caubl  24675  rrxdstprj1  24776  ovolshftlem2  24877  ovolicc2lem4  24887  uniioombl  24956  i1fmulclem  25070  mbfi1fseqlem6  25088  itg2const2  25109  itg2split  25117  bddiblnc  25209  ellimc2  25244  ellimc3  25246  limcflf  25248  dvmptfsum  25342  dvferm1  25352  dvferm2  25354  dvlip2  25362  c1lip1  25364  lhop1  25381  ftc1a  25404  ply1divex  25504  plyeq0lem  25574  plymullem1  25578  coemullem  25614  coemulc  25619  ulmshftlem  25751  ulmcaulem  25756  ulmbdd  25760  ulmcn  25761  ulmdvlem3  25764  mtestbdd  25767  pserulm  25784  pserdvlem2  25790  abelthlem8  25801  xrlimcnp  26321  jensen  26341  lgamucov  26390  logfac2  26568  dchrelbas3  26589  dchrpt  26618  gausslemma2dlem1a  26716  lgsquad3  26738  2sqb  26783  rpvmasumlem  26838  dchrisumlem1  26840  dchrisumlem3  26842  dchrmusum2  26845  dchrvmasumlem2  26849  dchrisum0flblem1  26859  dchrisum0lem1b  26866  dchrisum0lem1  26867  dchrisum0  26871  mulog2sumlem2  26886  pntlem3  26960  ostth3  26989  slerec  27161  cofcutr  27246  istrkgcb  27401  tgbtwndiff  27451  iscgrglt  27459  tgcgrxfr  27463  motcgrg  27489  lnext  27512  tgbtwnconn1  27520  tgbtwnconn3  27522  legval  27529  legtrid  27536  legso  27544  hlcgreu  27563  tglnne  27573  tglineeltr  27576  tglnne0  27585  colline  27594  tglowdim2l  27595  tglowdim2ln  27596  mirreu3  27599  mirbtwnhl  27625  krippenlem  27635  midexlem  27637  perpcom  27658  footexALT  27663  footex  27666  colperpexlem3  27677  colperpex  27678  opphllem  27680  midex  27682  oppne3  27688  opptgdim2  27690  oppnid  27691  opphllem2  27693  opphllem5  27696  opphllem6  27697  oppperpex  27698  outpasch  27700  hlpasch  27701  lnopp2hpgb  27708  hpgerlem  27710  colopp  27714  colhp  27715  lmieu  27729  lnperpex  27748  trgcopy  27749  trgcopyeulem  27750  iscgra1  27755  cgrane1  27757  cgrane2  27758  cgrane3  27759  cgrane4  27760  cgrahl1  27761  cgrahl2  27762  cgracgr  27763  cgraswap  27765  cgracom  27767  cgratr  27768  flatcgra  27769  cgrabtwn  27771  cgrahl  27772  sacgr  27776  acopyeu  27779  cgrg3col4  27798  tgasa1  27803  f1otrg  27816  f1otrge  27817  axeuclidlem  27914  axcontlem2  27917  umgrvad2edg  28164  usgredg2vlem2  28177  pthdepisspth  28686  clwwlkccatlem  28936  clwlkclwwlklem2  28947  3cycld  29125  eupth2lems  29185  eucrctshift  29190  frgr3vlem2  29221  n4cyclfrgr  29238  numclwwlk1lem2f1  29304  numclwwlk2lem1  29323  ubthlem3  29817  chirredlem1  31335  chirredlem3  31337  cdj1i  31378  fnpreimac  31590  xrge0infss  31668  nn0xmulclb  31679  hashxpe  31712  ccatf1  31808  swrdf1  31813  dfmgc2lem  31858  mgcf1o  31866  gsumhashmul  31901  xrge0tsmsd  31902  omndmul2  31923  gsumle  31935  psgnfzto1stlem  31952  cycpmco2  31985  cycpmrn  31995  tocyccntz  31996  cycpmconjslem2  32007  cyc3conja  32009  submarchi  32025  suborng  32113  isarchiofld  32115  imaslmod  32148  znfermltl  32158  lindfpropd  32172  nsgqusf1olem1  32194  ghmqusker  32201  rhmpreimaidl  32203  elrspunidl  32206  rhmimaidl  32209  qsidomlem1  32228  mxidlprm  32240  evls1fpws  32274  lindsunlem  32322  lindsun  32323  lbsdiflsp0  32324  dimkerim  32325  fedgmul  32329  extdg1id  32355  smatrcl  32380  1smat1  32388  submateq  32393  mdetpmtr1  32407  madjusmdetlem2  32412  locfinreflem  32424  cmppcmp  32442  rhmpreimacn  32469  ordtrest2NEWlem  32506  ordtconnlem1  32508  lmdvg  32537  esumpcvgval  32680  esum2d  32695  sigapildsys  32764  ldgenpisyslem1  32765  fiunelros  32776  volmeas  32833  imambfm  32865  omssubadd  32903  carsggect  32921  carsgclctunlem3  32923  sgnmul  33145  signsply0  33166  signstres  33190  actfunsnf1o  33220  actfunsnrndisj  33221  reprsuc  33231  reprinfz1  33238  breprexplema  33246  breprexplemc  33248  breprexp  33249  breprexpnat  33250  circlemeth  33256  hgt750lemb  33272  tgoldbachgtd  33278  erdszelem8  33795  pconnconn  33828  cvmlift2lem12  33911  cvmlift3lem5  33920  cvmlift3lem7  33922  cvmlift3lem8  33923  mrsubrn  34110  msrval  34135  msubff1  34153  btwnconn1lem13  34687  elicc3  34792  neibastop2lem  34835  unbdqndv2  34977  irrdifflemf  35799  ltflcei  36069  lindsenlbs  36076  matunitlindflem1  36077  matunitlindflem2  36078  poimirlem4  36085  poimirlem13  36094  poimirlem14  36095  poimirlem22  36103  poimirlem26  36107  poimirlem27  36108  heicant  36116  mblfinlem2  36119  mblfinlem3  36120  mblfinlem4  36121  cnambfre  36129  itg2addnclem  36132  itg2addnclem2  36133  itg2gt0cn  36136  ftc1cnnc  36153  ftc1anclem5  36158  ftc1anclem7  36160  ftc1anc  36162  equivtotbnd  36240  isbndx  36244  ssbnd  36250  heibor1lem  36271  rrncmslem  36294  islshpat  37482  lfl1dim  37586  lfl1dim2N  37587  lkrpssN  37628  glbconN  37842  glbconNOLD  37843  hlhgt2  37855  3dim2  37934  3dim3  37935  islln3  37976  islvol5  38045  2lplnja  38085  dalem19  38148  isline4N  38243  2polssN  38381  lhpmatb  38497  4atex  38542  trlatn0  38638  cdlemf2  39028  dialss  39512  diaglbN  39521  diaintclN  39524  dibglbN  39632  dibintclN  39633  dihlsscpre  39700  dihglblem5aN  39758  dihglblem2aN  39759  dihglblem4  39763  dihatexv  39804  dihjat1lem  39894  lcfl6  39966  mapdval2N  40096  aks4d1p8  40547  fldhmf1  40550  sticksstones8  40564  sticksstones12a  40568  imacrhmcl  40698  imadrhmcl  40719  fsuppind  40768  sn-0tie0  40911  prjspertr  40946  prjspreln0  40950  prjspner1  40967  elrfi  41020  eldioph2  41088  diophin  41098  irrapxlem2  41149  irrapxlem3  41150  irrapxlem4  41151  irrapxlem5  41152  pell1234qrne0  41179  pell1234qrreccl  41180  pell1234qrmulcl  41181  pell14qrgt0  41185  pell14qrdich  41195  pell1qrge1  41196  pellfundex  41212  congabseq  41301  jm2.27b  41333  jm2.27  41335  fnwe2lem2  41381  kelac1  41393  lnrfg  41449  hbt  41460  rfovcnvf1od  42283  ntrneiiso  42370  ntrneikb  42373  ntrneixb  42374  ntrneik3  42375  ntrneix3  42376  ntrneik13  42377  ntrneix13  42378  cvgdvgrat  42600  binomcxplemnotnn0  42643  sineq0ALT  43226  disjf1  43408  supxrgere  43574  supxrgelem  43578  supxrge  43579  suplesup  43580  xralrple2  43595  infxr  43608  infleinflem2  43612  infleinf  43613  uzub  43673  mccl  43846  limcrecl  43877  lptioo2  43879  lptioo1  43880  lptre2pt  43888  addlimc  43896  limsupmnflem  43968  climxrre  43998  liminflimsupclim  44055  climxlim2lem  44093  xlimliminflimsup  44110  icccncfext  44135  cncfiooicclem1  44141  cncfiooiccre  44143  dvbdfbdioolem2  44177  ioodvbdlimc1lem1  44179  dvnxpaek  44190  dvmptfprodlem  44192  dvmptfprod  44193  dvnprodlem3  44196  itgioocnicc  44225  itgspltprt  44227  stoweidlem31  44279  fourierdlem39  44394  fourierdlem42  44397  fourierdlem48  44402  fourierdlem49  44403  fourierdlem50  44404  fourierdlem51  44405  fourierdlem64  44418  fourierdlem65  44419  fourierdlem74  44428  fourierdlem75  44429  fourierdlem81  44435  fourierdlem82  44436  fourierdlem101  44455  etransclem23  44505  etransclem27  44509  etransclem32  44514  etransclem33  44515  etransclem35  44517  etransclem38  44520  sge0tsms  44628  sge0cl  44629  sge0f1o  44630  sge0split  44657  sge0rpcpnf  44669  sge0seq  44694  nnfoctbdjlem  44703  iundjiun  44708  meaiuninc3v  44732  meaiininclem  44734  omeiunltfirp  44767  carageniuncllem2  44770  carageniuncl  44771  hoidmv1lelem1  44839  hoidmvlelem3  44845  hoidmvlelem5  44847  hoidmvle  44848  hoiqssbllem3  44872  iunhoiioolem  44923  pimdecfgtioo  44965  pimincfltioo  44966  preimageiingt  44968  preimaleiinlt  44969  smflimlem4  45022  iccpartigtl  45622  iccpartgt  45626  sprsymrelf1lem  45690  paireqne  45710  proththd  45813  requad2  45822  sbgoldbst  45977  bgoldbtbndlem4  46007  isomushgr  46025  isomuspgrlem2d  46030  resmgmhm2b  46101  2zrngmmgm  46251  cznrng  46260  rnghmsubcsetclem2  46281  rhmsubcsetclem2  46327  srhmsubc  46381  rhmsubclem4  46394  srhmsubcALTV  46399  rhmsubcALTVlem4  46412  lincsum  46517  lcoss  46524  snlindsntor  46559  islindeps2  46571  line2x  46847  line2y  46848  itscnhlinecirc02p  46878
  Copyright terms: Public domain W3C validator