Theorem pm2.61i 126

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 124	. 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 127  pm2.61ii 130  pm2.61nii 131  pm2.61iii 132  pm2.61ian 476  pm5.21nii 679  biass 744  4cases 758  elimh 764  consensus 767  pm4.42 768  3ecase 923  equid 1126  dvelimfALT 1153  equvini 1168  ax11 1219  dfsb2 1225  sbn 1231  sbi1 1232  hbsb4 1248  sbidm 1254  sbco2 1255  sbco3 1257  sb9i 1263  ax11v 1265  hbs1 1332  hbsb 1333  sbal1 1346  sbal 1347  dvelimALT 1353  ax11inda2ALT 1369  ax11inda2 1370  a12lem1 1376  hbeu 1389  mo 1393  moexex 1438  2mo 1447  hbab 1467  pm2.61ine 1634  rgen2a 1699  ralcom2 1776  eueq2 1918  moeq3 1921  mo2icl 1923  sbc2or 1958  unineq 2255  noel 2284  ralidm 2357  ifid 2376  ifswap 2382  elimhyp 2390  elimhyp2v 2391  elimhyp3v 2392  elimhyp4v 2393  elimdhyp 2395  keephyp2v 2397  keephyp3v 2398  snsspr 2470  intabs 2733  class2set 2734  dtruALT 2748  snex 2750  dtru 2772  opth2 2800  dfid3 2836  unisn2 2875  nsuceq0 3053  trsuc 3055  ordsuc 3065  ordsucelsuc 3073  vtoclrbr 3212  vtoclibr 3213  relsn 3254  opeldm 3314  dmsnop 3328  soirri 3442  tz6.12-2 3739  ndmfv 3745  fveqres 3749  fvopabn 3786  eqfnfv 3797  fconst5 3848  rdgsucopabn 3947  elimdeloprv 4001  ndmoprcl 4044  ndmord 4050  1stval 4081  2ndval 4082  1st2val 4095  2nd2val 4096  om0x 4158  breng 4375  brdomg 4376  snfi 4432  snfiOLD 4433  unen 4434  pw2en 4446  ensdomtr 4471  sdomirr 4472  sdomen2 4482  pwuninel 4486  2pwuninel 4487  en2lp 4602  r1tr 4654  rankon 4671  r1pw 4686  r1pwcl 4687  rankuni 4698  scottex 4716  numth2 4785  cardval 4826  cardidm 4849  alephon 4865  alephcard 4867  alephnbtwn 4868  alephnbtwn2 4869  alephsucdom 4880  cfub 4908  cardcf 4911  cflecard 4912  cfle 4913  axunndlem1 4947  axpownd 4953  addcompi 5022  addasspi 5023  mulcompi 5024  mulasspi 5025  distrpi 5026  addnidpi 5028  nlt1pi 5033  addcompq 5062  addasspq 5063  mulcompq 5064  mulasspq 5065  distrpq 5067  genpass 5112  addcompr 5123  mulcompr 5125  distrpr 5132  ltexprlem7 5148  addcomsr 5196  addasssr 5197  mulcomsr 5198  mulasssr 5199  distrsr 5200  ndmioo 6370  iooid 6371  eliooret 6386  uzssz 6430  uzwo 6455  uzwoOLD 6456  elfzlem 6473  clmi1 7086  isumshft 7204  isumshft2 7205  ruclem13 7522  ruclem24 7533  ruclem26 7535  ruclem27 7536  ruclem28 7537  iooretop 7659  dscmet 7918  vafval 8222  bafval 8223  smfval 8224  0vfval 8225  vsfval 8254  avril1 8784  bcsALT 9046  lnopcon 9963  lnfncon 9990  elioo1t3 10496  oisbmi 10497  oisbmj 10498  hmeogrp 10538  cnfilca 10583  cnfilcaOLD 10584  domval 10655  codval 10656  idval 10657  cmpval 10658

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

Copyright terms: Public domain