Theorem pm2.61i 192

Description: Inference eliminating an antecedent.

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		pm2.61i.1	. . 3 |- (ph -> ps)
2		pm2.61i.2	. . 3 |- (-. ph -> ps)
3	1, 2	nsyl4 170	. 2 |- (-. ps -> ps)
4		pm2.18 129	. 2 |- ((-. ps -> ps) -> ps)
5	3, 4	ax-mp 7	1 |- ps

Syntax hints:  -. wn 2   -> wi 3

This theorem is referenced by:  pm2.61d 194  pm2.61ii 197  pm2.61nii 198  pm2.61niiOLD 199  pm2.61iii 200  jaoi 453  pm2.61ian 832  pm5.18 983  pm5.21nii 1005  biass 1057  ecase3 1067  4cases 1076  elimh 1084  pm4.42 1089  3ecase 1474  equid 1766  dvelimfALT 1794  exdistrf 1799  equveli 1812  ax11 1865  dfsb2 1871  sbn 1877  sbi1 1878  hbsb4 1895  sbco2 1902  sbco3 1904  sb9i 1910  ax11v 1912  hbs1 1985  hbsb 1986  sbal1 2001  sbal 2002  dvelimALT 2008  ax11inda2ALT 2024  ax11inda2 2025  a12lem1 2031  eujustALT 2040  hbeu 2048  mo 2053  moexex 2101  2mo 2110  hbab 2132  pm2.61ne 2338  pm2.61ine 2339  rgen2a 2411  ralcom2 2490  eueq2 2674  moeq3 2677  mo2icl 2679  sbc2or 2720  unineq 3053  noel 3086  ralidm 3172  ifid 3201  ifswap 3207  elimhyp 3215  elimhyp2v 3216  elimhyp3v 3217  elimhyp4v 3218  elimdhyp 3220  keephyp2v 3222  keephyp3v 3223  intabs 3637  class2set 3639  snex 3657  dtru 3662  dtruALT 3680  copsexg 3700  opth2 3709  dfid3 3748  nsuceq0 3891  ordsssuc2 3900  unisn2 3938  ordsuc 4038  ordsucelsuc 4045  vtoclrbr 4168  vtoclibr 4169  relsn 4218  opeldm 4286  soirri 4426  dmsnop 4472  tz6.12-2 4785  ndmfv 4788  fveqres 4793  dffv2 4820  fvopabn 4835  eqfnfv 4853  fconst5 4916  elimdeloprv 5023  ndmoprcl 5070  ndmord 5076  1stval 5128  2ndval 5129  1st2val 5144  2nd2val 5145  iotaex 5233  smofvon2 5267  rdgsucopabn 5319  om0x 5369  breng 5595  brdomg 5596  mapsnen 5650  snfi 5654  unen 5657  pw2en 5671  ensdomtr 5700  sdomirr 5701  sdomen2 5711  pwuninel 5719  2pwuninel 5720  riotav 5734  sucdom2 5810  unxpdomlem3 5819  fimax 5846  card2on 5926  en2lp 5939  r1tr 6001  rankon 6018  r1pw 6033  r1pwcl 6034  rankuni 6045  scottex 6085  cardval3 6104  cardon 6107  cardidm 6114  carden2b 6122  carddomi2 6125  alephon 6154  alephcard 6156  alephnbtwn 6157  onssnum 6207  cfub 6268  cardcf 6271  cflecard 6272  cfle 6273  cflim2 6283  cfidm 6290  axcc2lem 6293  numth2 6357  cardval 6389  cardidmOLD 6414  alephcardOLD 6431  alephnbtwnOLD 6432  alephnbtwn2OLD 6433  alephsucdomOLD 6441  alephreg 6449  pwcfsdom 6450  cfpwsdom 6451  axunndlem1 6465  axpownd 6471  addcompi 6540  addasspi 6541  mulcompi 6542  mulasspi 6543  distrpi 6544  addnidpi 6546  nlt1pi 6551  addcompq 6580  addasspq 6581  mulcompq 6582  mulasspq 6583  distrpq 6585  genpass 6630  addcompr 6641  mulcompr 6643  distrpr 6650  ltexprlem7 6666  addcomsr 6714  addasssr 6715  mulcomsr 6716  mulasssr 6717  distrsr 6718  ndmioo 7883  iooid 7884  elioore 7900  uzssz 7946  uzwo 7971  uzwoOLD 7972  elfzlem 8004  clmi1i 8742  isumshfti 8861  isumshft2i 8862  ruclem13 9185  ruclem24 9196  ruclem26 9198  ruclem27 9199  ruclem28 9200  gcdaddmlem 9328  indistop 9769  iooretop 9787  dscmet 10062  vafval 10423  bafval 10424  smfval 10425  0vfval 10426  vsfval 10455  vacnlem4 10539  avril1 11013  stoigOLD 11088  stoig 11089  ismgm 11205  bcsiALT 11515  lnopconi 12432  lnfnconi 12459  bnj1200 13748  trpredlem1 14579  bdayelon 14686  fldsqcp2 15088  elioo1t3 15599  oisbmi 15600  oisbmj 15601  oibbi1 15606  oibbi2 15607  hmeogrp 15649  subtopsin2 15669  subtopsin2OLD 15670  prtoptop 15684  cnfilca 15693  limfillem2 15705  domval 15864  codval 15865  idval 15866  cmpval 15867  cptarc 16052  topmtcl 16349  fvif 16516  fimaxOLD 16570  addcomgi 17277

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

Copyright terms: Public domain