Theorem pm2.61i 140

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 139	. 2 |- ((ph -> ps) -> ((-. ph -> ps) -> ps))
4	1, 2, 3	mp2 54	1 |- ps

Syntax hints:  -. wn 2   -> wi 3

This theorem is referenced by:  pm2.61d 141  pm2.61ii 144  pm2.61nii 145  pm2.61niiOLD 146  pm2.61iii 147  pm2.61ian 534  pm5.21nii 743  biass 816  4cases 832  elimh 841  consensusOLD 845  pm4.42 846  3ecase 1199  equid 1484  dvelimfALT 1514  equviniOLD 1532  ax11 1589  dfsb2 1595  sbn 1601  sbi1 1602  hbsb4 1620  sbidmOLD 1628  sbco2 1629  sbco3 1631  sb9i 1640  ax11v 1642  hbs1 1722  hbsb 1723  sbal1 1737  sbal 1738  dvelimALT 1744  ax11inda2ALT 1760  ax11inda2 1761  a12lem1 1767  eujustALT 1774  hbeu 1782  mo 1787  moexex 1841  2mo 1851  hbab 1875  pm2.61ne 2087  pm2.61ine 2089  pm2.61ineOLD 2090  rgen2a 2160  rgen2aOLD 2161  ralcom2 2244  ralcom2OLD 2245  eueq2 2429  moeq3 2432  mo2icl 2434  sbc2or 2481  unineq 2844  noel 2879  ralidm 2973  ifid 3003  ifswap 3010  elimhyp 3021  elimhyp2v 3022  elimhyp3v 3023  elimhyp4v 3024  elimdhyp 3026  keephyp2v 3028  keephyp3v 3029  snsspr1OLD 3136  intabs 3469  class2set 3471  snex 3492  snexOLD 3493  dtru 3498  dtruALT 3517  copsexg 3537  opth2 3546  dfid3 3587  nsuceq0 3749  trsucOLD 3753  ordsssuc2 3758  unisn2 3799  ordsuc 3895  ordsucelsuc 3902  ordsucelsucOLD 3903  vtoclrbr 4033  vtoclrbrOLD 4034  vtoclibr 4035  relsn 4087  opeldm 4160  soirri 4314  dmsnop 4367  dmsnopOLD 4368  tz6.12-2 4696  ndmfv 4702  nfunsnOLD 4707  fveqres 4708  dffv2 4734  fvopabn 4749  eqfnfv 4766  fconst5 4824  elimdeloprv 4930  ndmoprcl 4977  ndmord 4983  1stval 5022  2ndval 5023  1st2val 5038  2nd2val 5039  iotaex 5099  rdgsucopabn 5155  om0x 5203  breng 5434  brdomg 5435  snfi 5491  unen 5493  pw2en 5505  ensdomtr 5534  sdomirr 5535  sdomen2 5545  pwuninel 5550  2pwuninel 5551  riotav 5565  en2lp 5707  r1tr 5765  rankon 5782  r1pw 5797  r1pwcl 5798  rankuni 5809  scottex 5846  alephon 5876  numth2 5947  cardval 5975  cardidm 6001  alephcard 6015  alephnbtwn 6016  alephnbtwn2 6017  alephsucdom 6028  cfub 6056  cardcf 6059  cflecard 6060  cfle 6061  axunndlem1 6099  axpownd 6105  addcompi 6174  addasspi 6175  mulcompi 6176  mulasspi 6177  distrpi 6178  addnidpi 6180  nlt1pi 6185  addcompq 6214  addasspq 6215  mulcompq 6216  mulasspq 6217  distrpq 6219  genpass 6264  addcompr 6275  mulcompr 6277  distrpr 6284  ltexprlem7 6300  addcomsr 6348  addasssr 6349  mulcomsr 6350  mulasssr 6351  distrsr 6352  ndmioo 7537  iooid 7538  elioore 7554  uzssz 7599  uzwo 7624  uzwoOLD 7625  elfzlem 7643  clmi1i 8346  isumshfti 8465  isumshft2i 8466  ruclem13 8791  ruclem24 8802  ruclem26 8804  ruclem27 8805  ruclem28 8806  indistop 8918  iooretop 8929  dscmet 9196  vafval 9554  bafval 9555  smfval 9556  0vfval 9557  vsfval 9586  vacnlem4 9670  avril1 10142  stoig 10251  ismgm 10367  bcsiALT 10679  lnopconi 11600  lnfnconi 11627  bnj1200 12977  gcdaddmlem 13734  trcllem1 13933  bdayelon 14017  fldsqcp2 14378  elioo1t3 14846  oisbmi 14847  oisbmj 14848  oibbi1 14853  oibbi2 14854  hmeogrp 14892  subtopsin2 14907  prtoptop 14919  cnfilca 14927  limfillem2 14939  domval 15070  codval 15071  idval 15072  cmpval 15073  cptarc 15242  topmtcl 15525  fvif 15692  fimax 15746  addcomgi 16455

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

Copyright terms: Public domain