Theorem pm2.61i 124

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	. 2 |- (ph -> ps)
2		pm2.61i.2	. 2 |- (-. ph -> ps)
3		pm2.61 123	. 2 |- ((ph -> ps) -> ((-. ph -> ps) -> ps))
4	1, 2, 3	mp2 43	1 |- ps

Syntax hints:  -. wn 2   -> wi 3

This theorem is referenced by:  pm2.61d 125  pm2.61ii 128  pm2.61nii 129  pm2.61iii 130  pm2.61ian 479  pm5.21nii 683  biass 749  4cases 763  elimh 769  consensus 772  pm4.42 773  3ecase 930  equid 1162  dvelimfALT 1190  equvini 1205  ax11 1256  dfsb2 1262  sbn 1268  sbi1 1269  hbsb4 1286  sbidm 1292  sbco2 1293  sbco3 1295  sb9i 1301  ax11v 1303  hbs1 1371  hbsb 1372  sbal1 1385  sbal 1386  dvelimALT 1392  ax11inda2ALT 1408  ax11inda2 1409  a12lem1 1415  hbeu 1428  mo 1432  moexex 1478  2mo 1487  hbab 1509  pm2.61ine 1680  rgen2a 1745  ralcom2 1822  eueq2 1964  moeq3 1967  mo2icl 1969  sbc2or 2006  unineq 2307  noel 2336  ralidm 2411  ifid 2430  ifswap 2436  elimhyp 2447  elimhyp2v 2448  elimhyp3v 2449  elimhyp4v 2450  elimdhyp 2452  keephyp2v 2454  keephyp3v 2455  snsspr1 2534  intabs 2807  class2set 2808  snex 2826  dtru 2831  dtruALT 2848  opth2 2876  dfid3 2914  nsuceq0 3053  trsuc 3056  unisn2 3098  ordsuc 3171  ordsucelsuc 3178  vtoclrbr 3295  vtoclibr 3296  relsn 3343  opeldm 3405  soirri 3534  dmsnop 3577  tz6.12-2 3850  ndmfv 3856  fveqres 3860  fvopabn 3897  eqfnfv 3909  eqfnfv2 3911  fconst5 3962  elimdeloprv 4061  ndmoprcl 4105  ndmord 4111  1stval 4142  2ndval 4143  1st2val 4158  2nd2val 4159  rdgsucopabn 4248  om0x 4294  breng 4516  brdomg 4517  snfi 4573  unen 4575  pw2en 4587  ensdomtr 4616  sdomirr 4617  sdomen2 4627  pwuninel 4631  2pwuninel 4632  en2lp 4747  r1tr 4800  rankon 4817  r1pw 4832  r1pwcl 4833  rankuni 4844  scottex 4862  numth2 4931  cardval 4973  cardidm 4999  alephon 5015  alephcard 5017  alephnbtwn 5018  alephnbtwn2 5019  alephsucdom 5030  cfub 5058  cardcf 5061  cflecard 5062  cfle 5063  axunndlem1 5101  axpownd 5107  addcompi 5176  addasspi 5177  mulcompi 5178  mulasspi 5179  distrpi 5180  addnidpi 5182  nlt1pi 5187  addcompq 5216  addasspq 5217  mulcompq 5218  mulasspq 5219  distrpq 5221  genpass 5266  addcompr 5277  mulcompr 5279  distrpr 5286  ltexprlem7 5302  addcomsr 5350  addasssr 5351  mulcomsr 5352  mulasssr 5353  distrsr 5354  ndmioo 6496  iooid 6497  elioore 6512  uzssz 6557  uzwo 6582  uzwoOLD 6583  elfzlem 6601  clmi1i 7289  isumshfti 7408  isumshft2i 7409  ruclem13 7734  ruclem24 7745  ruclem26 7747  ruclem27 7748  ruclem28 7749  indistop 7860  iooretop 7869  dscmet 8129  vafval 8469  bafval 8470  smfval 8471  0vfval 8472  vsfval 8501  vacnlem4 8585  avril1 9058  bcsiALT 9322  lnopconi 10242  lnfnconi 10269  fldsqcp2 10780  ismgm 10897  elioo1t3 10996  oisbmi 10997  oisbmj 10998  oibbi1 11004  oibbi2 11005  hmeogrp 11044  stoig 11064  subtopsin2 11067  cnfilca 11088  limfillem2 11102  domval 11177  codval 11178  idval 11179  cmpval 11180  topmtcl 11586  fvif 11799  fimax 11837

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

Copyright terms: Public domain