Theorem pm2.61i 132

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 130	. 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 133  pm2.61ii 136  pm2.61nii 137  pm2.61iii 138  pm2.61ian 487  pm5.21nii 691  biass 756  4cases 770  elimh 776  consensus 779  pm4.42 780  3ecase 935  equid 1167  dvelimfALT 1195  equvini 1210  ax11 1261  dfsb2 1267  sbn 1273  sbi1 1274  hbsb4 1290  sbidm 1296  sbco2 1297  sbco3 1299  sb9i 1305  ax11v 1307  hbs1 1374  hbsb 1375  sbal1 1388  sbal 1389  dvelimALT 1395  ax11inda2ALT 1411  ax11inda2 1412  a12lem1 1418  hbeu 1431  mo 1435  moexex 1481  2mo 1490  hbab 1513  pm2.61ine 1681  rgen2a 1746  ralcom2 1823  eueq2 1965  moeq3 1968  mo2icl 1970  sbc2or 2008  unineq 2306  noel 2335  ralidm 2409  ifid 2428  ifswap 2434  elimhyp 2442  elimhyp2v 2443  elimhyp3v 2444  elimhyp4v 2445  elimdhyp 2447  keephyp2v 2449  keephyp3v 2450  snsspr 2524  intabs 2788  class2set 2789  dtruALT 2804  snex 2806  dtru 2828  opth2 2856  dfid3 2892  unisn2 2931  nsuceq0 3110  trsuc 3112  ordsuc 3122  ordsucelsuc 3130  vtoclrbr 3269  vtoclibr 3270  relsn 3311  opeldm 3371  dmsnop 3385  soirri 3499  tz6.12-2 3796  ndmfv 3802  fveqres 3806  fvopabn 3843  eqfnfv 3854  fconst5 3905  rdgsucopabn 4005  elimdeloprv 4059  ndmoprcl 4102  ndmord 4108  1stval 4139  2ndval 4140  1st2val 4153  2nd2val 4154  om0x 4216  breng 4436  brdomg 4437  snfi 4493  unen 4497  pw2en 4509  ensdomtr 4534  sdomirr 4535  sdomen2 4545  pwuninel 4549  2pwuninel 4550  en2lp 4664  r1tr 4716  rankon 4733  r1pw 4748  r1pwcl 4749  rankuni 4760  scottex 4778  numth2 4847  cardval 4889  cardidm 4914  alephon 4930  alephcard 4932  alephnbtwn 4933  alephnbtwn2 4934  alephsucdom 4945  cfub 4973  cardcf 4976  cflecard 4977  cfle 4978  axunndlem1 5012  axpownd 5018  addcompi 5087  addasspi 5088  mulcompi 5089  mulasspi 5090  distrpi 5091  addnidpi 5093  nlt1pi 5098  addcompq 5127  addasspq 5128  mulcompq 5129  mulasspq 5130  distrpq 5132  genpass 5177  addcompr 5188  mulcompr 5190  distrpr 5197  ltexprlem7 5213  addcomsr 5261  addasssr 5262  mulcomsr 5263  mulasssr 5264  distrsr 5265  ndmioo 6395  iooid 6396  elioore 6411  uzssz 6456  uzwo 6481  uzwoOLD 6482  elfzlem 6499  clmi1i 7176  isumshfti 7294  isumshft2i 7295  ruclem13 7614  ruclem24 7625  ruclem26 7627  ruclem27 7628  ruclem28 7629  indistop 7735  iooretop 7744  dscmet 8003  vafval 8306  bafval 8307  smfval 8308  0vfval 8309  vsfval 8338  avril1 8867  bcsiALT 9129  lnopconi 10046  lnfnconi 10073  elioo1t3 10590  oisbmi 10591  oisbmj 10592  hmeogrp 10632  cnfilca 10670  domval 10737  codval 10738  idval 10739  cmpval 10740

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

Copyright terms: Public domain