MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  pm2.61i Unicode version

Theorem pm2.61i 158
Description: Inference eliminating an antecedent. (Contributed by NM, 5-Apr-1994.) (Proof shortened by Wolf Lammen, 12-Sep-2013.)
Hypotheses
Ref Expression
pm2.61i.1  |-  ( ph  ->  ps )
pm2.61i.2  |-  ( -. 
ph  ->  ps )
Assertion
Ref Expression
pm2.61i  |-  ps

Proof of Theorem pm2.61i
StepHypRef Expression
1 id 20 . 2  |-  ( ph  ->  ph )
2 pm2.61i.2 . . 3  |-  ( -. 
ph  ->  ps )
3 pm2.61i.1 . . 3  |-  ( ph  ->  ps )
42, 3ja 155 . 2  |-  ( (
ph  ->  ph )  ->  ps )
51, 4ax-mp 8 1  |-  ps
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4
This theorem is referenced by:  pm2.61ii  159  pm2.61nii  160  pm2.61iii  161  pm2.65i  167  pm5.21nii  343  pm5.18  346  biass  349  pm2.61ian  766  ecase3  908  4cases  916  elimh  923  pm4.42  927  3ecase  1288  a9e  1941  ax9OLD  1989  dvelimh  2003  exdistrf  2010  equveli  2023  dfsb2  2088  sbn  2095  sbi1  2096  sbco2  2119  sbco3  2121  sb9i  2127  ax11v  2129  hbs1  2138  nfsb  2142  sbal1  2160  sbal  2161  dvelimALT  2167  ax11  2189  equid1  2192  equid1ALT  2210  dvelimf-o  2214  ax11inda2ALT  2232  ax11inda2  2233  eujustALT  2241  moexex  2307  pm2.61ne  2625  pm2.61ine  2626  rgen2a  2715  ralcom2  2815  eueq2  3051  moeq3  3054  mo2icl  3056  sbc2or  3112  unineq  3534  ralidm  3674  ifsb  3691  ifid  3714  ifnot  3720  ifan  3721  ifor  3722  elimhyp  3730  elimhyp2v  3731  elimhyp3v  3732  elimhyp4v  3733  elimdhyp  3735  keephyp2v  3737  keephyp3v  3738  rabrsn  3817  tppreqb  3882  ssunsn2  3901  dfopif  3923  intabs  4302  class2set  4308  snexALT  4326  dtru  4331  dtruALT  4337  snex  4346  dtruALT2  4349  copsexg  4383  dfid3  4440  nsuceq0  4602  ordsssuc2  4610  unisn2  4651  ordsuc  4734  ordsucelsuc  4742  soirri  5200  soirriOLD  5205  dmsnopss  5282  dmsnsnsn  5288  opswap  5296  unixpid  5344  iotassuni  5374  iotaex  5375  dfiota4  5386  dffv3  5664  fvrn0  5693  ndmfv  5695  fveqres  5703  dffv2  5735  fvco4i  5740  fvmptss  5752  fvmptex  5754  fvmptss2  5763  f0cli  5819  fvunsn  5864  fconst5  5888  0neqopab  6058  elimdelov  6092  ndmovcl  6171  ndmovord  6176  1stval  6290  2ndval  6291  1st2val  6311  2nd2val  6312  bropopvvv  6365  mpt2xopynvov0  6405  mpt2xopoveqd  6408  pwuninel  6481  riotav  6490  riotassuni  6524  smofvon2  6554  om0x  6699  brdomg  7054  snfi  7123  sdomirr  7180  domunsn  7193  2pwuninel  7198  fipwuni  7366  oicl  7431  oif  7432  card2on  7455  en2lp  7504  tctr  7612  r1tr  7635  rankdmr1  7660  r1pw  7704  r1pwOLD  7705  rankuni  7722  scottex  7742  cardidm  7779  alephcard  7884  alephnbtwn  7885  cdacomen  7994  cfub  8062  cardcf  8065  cflecard  8066  cfle  8067  cflim2  8076  cfidm  8088  isf32lem9  8174  itunisuc  8232  itunitc1  8233  itunitc  8234  ituniiun  8235  axcc2lem  8249  alephreg  8390  pwcfsdom  8391  cfpwsdom  8392  axunndlem1  8403  axpownd  8409  tskmcl  8649  addcompi  8704  addasspi  8705  mulcompi  8706  mulasspi  8707  distrpi  8708  addnidpi  8711  nlt1pi  8716  addcompq  8760  addcomnq  8761  mulcompq  8762  mulcomnq  8763  adderpq  8766  mulerpq  8767  addassnq  8768  mulassnq  8769  distrnq  8771  genpass  8819  addcompr  8831  mulcompr  8833  distrpr  8838  ltexprlem7  8852  addcomsr  8895  addasssr  8896  mulcomsr  8897  mulasssr  8898  distrsr  8899  uzssz  10437  uzwo  10471  uzwoOLD  10472  elixx3g  10861  iooid  10876  elfz2  10982  injresinjlem  11126  injresinj  11127  ltweuz  11228  fzofi  11240  hashrabrsn  11575  elprchashprn2  11594  hashsnlei  11607  hash1snb  11608  hashgt12el  11609  hashgt12el2  11610  swrd00  11692  gcdaddmlem  12955  pcmptcl  13187  strfvss  13414  strfvi  13434  setsnid  13436  ressbas  13446  ressbasss  13448  resslem  13449  ress0  13450  ressress  13453  strle1  13487  0rest  13584  firest  13587  topnval  13589  xpsaddlem  13727  xpsvsca  13731  homffval  13844  comfffval  13851  oppchomfval  13867  oppcbas  13871  fullfunc  14030  fthfunc  14031  natfval  14070  fucbas  14084  fuchom  14085  arwval  14125  coafval  14146  xpcbas  14202  xpchomfval  14203  xpccofval  14206  oduval  14484  oduleval  14485  odumeet  14494  odujoin  14496  ipopos  14513  plusffval  14629  grpidval  14634  gsum0  14707  frmdplusg  14726  frmd0  14732  grpinvfval  14770  grpinvfvi  14773  grpsubfval  14774  mulgfval  14818  mulgfvi  14821  symgbas  15022  symgplusg  15026  cntrval  15045  oppgval  15070  oppgplusfval  15071  odfval  15098  oppglsm  15203  efgval  15276  mgpval  15578  mgpplusg  15579  rngidval  15593  opprval  15656  opprmulfval  15657  dvdsrval  15677  invrfval  15705  dvrfval  15716  staffval  15862  scaffval  15895  rlmval  16191  rlmsca2  16199  2idlval  16231  rrgval  16274  asclfval  16320  psrplusg  16372  psrmulr  16375  psrvscafval  16381  mplval  16419  mplcoe3  16456  psr1val  16511  vr1val  16517  ply1val  16519  ply1basfvi  16562  ply1plusgfvi  16563  psr1sca2  16572  ply1sca2  16575  ply1ascl  16578  zrhval  16712  zlmlem  16721  zlmvsca  16726  chrval  16729  ipffval  16802  thlbas  16846  thlle  16847  thloc  16849  pjfval  16856  tgdif0  16980  indislem  16987  resstopn  17172  iocpnfordt  17201  icomnfordt  17202  hmeofval  17711  ussval  18210  nmfval  18507  nghmfval  18627  pcofval  18906  tchval  19048  ioombl  19326  ibladdlem  19578  itgaddlem1  19581  iblabs  19587  limccnp2  19646  dvbsss  19656  perfdvf  19657  evlval  19812  evl1fval  19814  mdegfval  19852  deg1fval  19870  deg1fvi  19875  uc1pval  19929  mon1pval  19931  usgraedgprv  21263  usgra1v  21275  nbusgra  21306  nbgra0nb  21307  nbgranself2  21314  cusgra1v  21336  uvtxisvtx  21365  uvtx0  21366  uvtx01vtx  21367  1conngra  21510  vdgrf  21517  avril1  21605  ismgm  21756  vafval  21930  bafval  21931  smfval  21932  vsfval  21962  bcsiALT  22529  cntnevol  24376  dfrdg3  25177  trpredlem1  25254  bdayelon  25358  unisnif  25488  funpartfv  25508  fullfunfv  25510  axcontlem12  25628  linedegen  25791  itg2addnclem  25957  ibladdnclem  25961  itgaddnclem1  25963  iblabsnc  25969  iblmulc2nc  25970  mzpmfp  26495  dsmmval2  26871  itgocn  27038  psgnfval  27092  mdetfval  27156  mendbas  27161  mendplusgfval  27162  mendmulrfval  27164  mendsca  27166  mendvscafval  27167  addcomgi  27329  tz6.12-afv  27706  ndmaovcl  27736  frgra2v  27752  1to2vfriswmgra  27759  2pthfrgra  27764  frgrancvvdeqlem2  27783  a9e2ndeq  27989  2sb5ndVD  28363  2sb5ndALT  28386  bnj1189  28716  ax9NEW7  28806  dvelimhvAUX7  28830  exdistrfNEW7  28843  equveliNEW7  28864  sbnNEW7  28898  sbi1NEW7  28899  sbco2wAUX7  28920  sbco3wAUX7  28922  ax11vNEW7  28928  hbs1NEW7  28938  sbal1NEW7  28948  sbalNEW7  28949  dvelimALTNEW7  28969  dfsb2NEW7  28971  ax7w2AUX7  28982  ax7w6AUX7  28984  dvelimhOLD7  29029  nfsbOLD7  29064  sbco2OLD7  29068  sbco3OLD7  29070  sb9iOLD7  29074
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
  Copyright terms: Public domain W3C validator