Theorem pm2.61i 176

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

Step	Hyp	Ref	Expression
1		id 22	. 2 |- ( ph -> ph )
2		pm2.61i.2	. . 3 |- ( -. ph -> ps )
3		pm2.61i.1	. . 3 |- ( ph -> ps )
4	2, 3	ja 173	. 2 |- ( ( ph -> ph ) -> ps )
5	1, 4	ax-mp 5	1 |- ps

Syntax hints:   -. wn 3   -> wi 4

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem is referenced by:  pm2.61ii  177  pm2.61nii  178  pm2.61iii  179  pm2.65i  185  pm5.21nii  368  pm5.18  371  biass  374  pm2.61ian  831  ecase3  982  4cases  990  pm4.42  1004  ifpid  1025  elimh  1030  elimhOLD  1033  3ecase  1437  ax6e  2250  ax12  2304  exdistrf  2333  ax12OLD  2341  equvini  2346  dfsb2  2373  sbequi  2375  sbi1  2392  sbcom3  2411  sbco2  2415  sbco3  2417  sb9  2426  ax12vALT  2428  hbs1  2436  nfsb  2440  2ax6e  2450  sbal  2462  eujustALT  2473  pm2.61ine  2877  ralcom2  3104  eueq2  3380  moeq3  3383  mo2icl  3385  sbc2or  3444  sbcimdvOLD  3499  unineq  3877  csb0  3982  sbcel12  3983  sbcne12  3986  sbcel2  3989  csbidm  4002  csbun  4009  csbin  4010  ralidm  4075  ifsb  4099  ifid  4125  ifnot  4133  ifan  4134  ifor  4135  csbif  4138  elimhyp  4146  elimhyp2v  4147  elimhyp3v  4148  elimhyp4v  4149  elimdhyp  4151  keephyp2v  4153  keephyp3v  4154  eqoreldifOLD  4226  rabsnif  4258  tppreqb  4336  ssunsn2  4359  n0snor2el  4364  elpreqprlem  4395  dfopif  4399  csbuni  4466  disjord  4641  sbcbr  4707  unisn2  4794  intabs  4825  class2set  4832  snexALT  4852  dtru  4857  dtruALT  4899  snex  4908  dtruALT2  4911  copsexg  4956  csbopab  5008  dfid3  5025  csbxp  5200  csbres  5399  csbima12  5483  soirri  5522  csbrn  5596  dmsnopss  5607  dmsnsnsn  5613  opswap  5622  unixpid  5670  nsuceq0  5805  ordsssuc2  5814  iotassuni  5867  iotaex  5868  dfiota4OLD  5880  csbiota  5881  dffv3  6187  fvrn0  6216  ndmfv  6218  elfv2ex  6229  fveqres  6230  csbfv12  6231  csbfv  6233  dffv2  6271  fvco4i  6276  fvmptss  6292  fvmptex  6294  fvmptss2  6304  f0cli  6370  fvunsn  6445  fconst5  6471  csbriota  6623  riotassuni  6648  csbov123  6687  csbov  6688  fvmptopab  6697  0neqopab  6698  brfvopab  6700  elimdelov  6736  ovif12  6739  ndmovcl  6819  ndmovord  6824  elovmpt3imp  6890  difsnexi  6970  ordsuc  7014  ordsucelsuc  7022  1stval  7170  2ndval  7171  1st2val  7194  2nd2val  7195  el2mpt2csbcl  7250  bropopvvv  7255  bropfvvvvlem  7256  bropfvvvv  7257  suppimacnv  7306  suppssdm  7308  ressuppss  7314  suppun  7315  extmptsuppeq  7319  funsssuppss  7321  fczsupp0  7324  suppss  7325  suppssov1  7327  suppss2  7329  suppssfv  7331  supp0cosupp0  7334  imacosupp  7335  mpt2xopynvov0  7344  mpt2xopoveqd  7347  pwuninel  7401  smofvon2  7453  om0x  7599  brdomg  7965  snfi  8038  sdomirr  8097  domunsn  8110  2pwuninel  8115  snnen2o  8149  suppeqfsuppbi  8289  fsuppun  8294  funsnfsupp  8299  fipwuni  8332  oicl  8434  oif  8435  wemapso2  8458  card2on  8459  en2lp  8510  tctr  8616  r1tr  8639  rankdmr1  8664  r1pw  8708  r1pwALT  8709  rankuni  8726  scottex  8748  cardidm  8785  alephcard  8893  alephnbtwn  8894  cdacomen  9003  cfub  9071  cardcf  9074  cflecard  9075  cfle  9076  cflim2  9085  cfidm  9097  isf32lem9  9183  itunisuc  9241  itunitc1  9242  itunitc  9243  ituniiun  9244  axcc2lem  9258  alephreg  9404  pwcfsdom  9405  cfpwsdom  9406  axunndlem1  9417  axpownd  9423  tskmcl  9663  addcompi  9716  addasspi  9717  mulcompi  9718  mulasspi  9719  distrpi  9720  addnidpi  9723  nlt1pi  9728  addcompq  9772  addcomnq  9773  mulcompq  9774  mulcomnq  9775  adderpq  9778  mulerpq  9779  addassnq  9780  mulassnq  9781  distrnq  9783  genpass  9831  addcompr  9843  mulcompr  9845  distrpr  9850  ltexprlem7  9864  addcomsr  9908  addasssr  9909  mulcomsr  9910  mulasssr  9911  distrsr  9912  uzssz  11707  uzwo  11751  nn01to3  11781  xnn0xaddcl  12066  elixx3g  12188  iooid  12203  elfz2  12333  injresinjlem  12588  injresinj  12589  fleqceilz  12653  modifeq2int  12732  modfzo0difsn  12742  addmodlteq  12745  ltweuz  12760  fzofi  12773  fsuppmapnn0fiubex  12792  hashrabrsn  13161  hashrabsn01  13162  hashrabsn1  13163  elprchashprn2  13184  hashss  13197  hashsn01  13204  hash1snb  13207  hashgt12el  13210  hashgt12el2  13211  hashfzp1  13218  hash2pwpr  13258  hashge2el2dif  13262  ccatsymb  13366  swrd00  13418  swrd0  13434  swrdccatin1  13483  repswswrd  13531  0csh0  13539  cshwcl  13544  cshwidxmod  13549  repswcshw  13558  cshw1  13568  s3sndisj  13706  s3iunsndisj  13707  xptrrel  13719  trclfvcotrg  13757  relexpfld  13789  modfsummods  14525  pwm1geoser  14600  dvdsaddre2b  15029  gcdaddmlem  15245  prm23ge5  15520  pcmptcl  15595  prmgaplem5  15759  prmgaplem6  15760  cshwshash  15811  strfvss  15880  strfvi  15913  setsnid  15915  ressbas  15930  ressbasss  15932  resslem  15933  ress0  15934  ressress  15938  strle1  15973  0rest  16090  firest  16093  topnval  16095  xpsaddlem  16235  xpsvsca  16239  homffval  16350  comfffval  16358  oppchomfval  16374  oppcbas  16378  fullfunc  16566  fthfunc  16567  natfval  16606  fucbas  16620  fuchom  16621  arwval  16693  coafval  16714  xpcbas  16818  xpchomfval  16819  xpccofval  16822  lubfun  16980  glbfun  16993  oduval  17130  oduleval  17131  odumeet  17140  odujoin  17142  ipopos  17160  plusffval  17247  grpidval  17260  gsum0  17278  frmdplusg  17391  frmd0  17397  mgm2nsgrplem2  17406  mgm2nsgrplem3  17407  sgrp2rid2  17413  dfgrp2e  17448  grpinvfval  17460  grpinvfvi  17463  grpsubfval  17464  mulgfval  17542  mulgfvi  17545  cntrval  17752  oppgval  17777  oppgplusfval  17778  symgbas  17800  symgplusg  17809  psgnfval  17920  odfval  17952  oppglsm  18057  efgval  18130  mgpval  18492  mgpplusg  18493  ringidval  18503  opprval  18624  opprmulfval  18625  dvdsrval  18645  invrfval  18673  dvrfval  18684  staffval  18847  scaffval  18881  rlmval  19191  rlmsca2  19201  2idlval  19233  rrgval  19287  asclfval  19334  psrplusg  19381  psrmulr  19384  psrvscafval  19390  mplval  19428  mplcoe3  19466  evlval  19524  psr1val  19556  vr1val  19562  ply1val  19564  ply1basfvi  19611  ply1plusgfvi  19612  psr1sca2  19621  ply1sca2  19624  ply1ascl  19628  cply1mul  19664  gsummoncoe1  19674  evl1fval  19692  evl1fval1  19695  zrhval  19856  zlmlem  19865  zlmvsca  19870  chrval  19873  evpmss  19932  psgndiflemB  19946  ipffval  19993  thlbas  20040  thlle  20041  thloc  20043  pjfval  20050  dsmmval2  20080  mamufacex  20195  mavmulsolcl  20357  marrepfval  20366  marepvfval  20371  submafval  20385  mdetfval  20392  mdetfval1  20396  mdetunilem7  20424  mdetunilem8  20425  madufval  20443  minmar1fval  20452  mp2pm2mplem4  20614  toponsspwpw  20726  tgdif0  20796  indislem  20804  resstopn  20990  iocpnfordt  21019  icomnfordt  21020  hmeofval  21561  ussval  22063  nmfval  22393  nghmfval  22526  pcofval  22810  tchval  23017  ioombl  23333  ibladdlem  23586  itgaddlem1  23589  iblabs  23595  dvbsss  23666  perfdvf  23667  mdegfval  23822  deg1fval  23840  deg1fvi  23845  uc1pval  23899  mon1pval  23901  lgsqrmodndvds  25078  gausslemma2dlem1a  25090  2lgs  25132  ttglem  25756  axcontlem12  25855  vtxval  25878  iedgval  25879  edgval  25941  usgr1v  26148  nbuhgr  26239  nbumgr  26243  uhgrnbgr0nb  26250  nbgr1vtx  26254  nbgrnself2  26259  nbusgrvtxm1  26281  uvtxa0  26294  sizusglecusg  26359  g0wlk0  26548  wlkreslem  26566  lfgrwlkprop  26584  wwlks  26727  wwlksn  26729  wspthsn  26735  iswwlksnon  26740  iswspthsnon  26741  0enwwlksnge1  26749  wwlksnfi  26801  wwlksnonfi  26816  wspn0  26820  wwlks2onv  26847  clwwlks  26879  clwwlksn  26881  clwlkclwwlklem2a4  26898  umgrclwwlksge2  26912  clwwlksnfi  26913  1conngr  27054  eupth2lem3lem7  27094  frgr1v  27135  nfrgr2v  27136  1to2vfriswmgr  27143  2wspmdisj  27201  frgrreggt1  27251  frgrreg  27252  frgrregord013  27253  frgrogt3nreg  27255  friendship  27257  avril1  27319  vafval  27458  bafval  27459  smfval  27460  vsfval  27488  bcsiALT  28036  resvsca  29830  resvlem  29831  cntnevol  30291  signsw0glem  30630  bnj1189  31077  mvtval  31397  mexval  31399  mexval2  31400  mdvval  31401  mrsubfval  31405  mrsubrn  31410  msubfval  31421  elmsubrn  31425  msubrn  31426  mvhfval  31430  mpstval  31432  msrfval  31434  mstaval  31441  mppsval  31469  mthmval  31472  dfrdg3  31702  trpredlem1  31727  fvsingle  32027  unisnif  32032  funpartfv  32052  fullfunfv  32054  linedegen  32250  bj-ax6e  32653  axc11n11r  32673  bj-ax12v3ALT  32676  bj-dtru  32797  bj-sbsb  32824  bj-nfcsym  32886  bj-restsnid  33040  bj-inftyexpidisj  33097  csbdif  33171  finxpreclem4  33231  finxp00  33239  wl-nfs1t  33324  wl-sbcom3  33372  matunitlindflem1  33405  itg2addnclem  33461  ibladdnclem  33466  itgaddnclem1  33468  iblabsnc  33474  iblmulc2nc  33475  ftc1anclem8  33492  ismgmOLD  33649  tsbi1  33940  tsbi2  33941  ac6s6  33980  equid1  34184  ax12fromc15  34190  equid1ALT  34210  dvelimf-o  34214  ax12inda2ALT  34231  ax12inda2  34232  mzpmfp  37310  itgocn  37734  mendbas  37754  mendplusgfval  37755  mendmulrfval  37757  mendsca  37759  mendvscafval  37760  arearect  37801  areaquad  37802  or3or  38319  uneqsn  38321  addcomgi  38660  ax6e2ndeq  38775  2sb5ndVD  39146  2sb5ndALT  39168  sqwvfoura  40445  sqwvfourb  40446  fourierswlem  40447  fouriersw  40448  hspdifhsp  40830  hspmbllem2  40841  hspmbl  40843  tz6.12-afv  41253  ndmaovcl  41283  otiunsndisjX  41298  nltle2tri  41323  fzopredsuc  41333  iccpartiltu  41358  iccpartigtl  41359  iccpartlt  41360  icceuelpartlem  41371  iccpartnel  41374  pfx00  41384  pfx0  41385  fmtnoprmfac1  41477  fmtnoprmfac2  41479  prmdvdsfmtnof1lem2  41497  prminf2  41500  lighneallem4  41527  evenprm2  41623  even3prm2  41628  stgoldbwt  41664  upwlkbprop  41719  elsprel  41725  sprssspr  41731  sprsymrelfvlem  41740  nzerooringczr  42072  pgrpgt2nabl  42147  suppmptcfin  42160  linc1  42214  lindslinindsimp2lem5  42251  setrec2lem1  42440