Theorem pm2.43i 64

Description: Inference absorbing redundant antecedent. (The proof was shortened by O'Cat, 28-Nov-2008.)

Hypothesis

Ref	Expression
pm2.43i.1	|- (ph -> (ph -> ps))

Assertion

Ref	Expression
pm2.43i	|- (ph -> ps)

Proof of Theorem pm2.43i

Step	Hyp	Ref	Expression
1		id 59	. 2 |- (ph -> ph)
2		pm2.43i.1	. 2 |- (ph -> (ph -> ps))
3	1, 2	mpd 26	1 |- (ph -> ps)

Syntax hints:   -> wi 3

This theorem is referenced by:  pm2.18 81  anidm 433  anidms 435  anabsi5 498  ibi 595  3anidm12 888  ax4 1008  equid 1162  equidALT 1163  ax10 1178  hbae 1182  equid1 1307  ax11inda 1410  vtoclgaf 1897  sbcth2 2030  ssiun2s 2662  copsexg 2868  tz7.7 3001  nsuceq0 3053  reuuni2f 3107  oprabvalig 4084  tfrlem9 4220  tfrlem11 4222  omcl 4307  oecl 4308  odi 4346  nnmcl 4370  nnecl 4371  sbth 4602  zorn2lem6 4939  zorn2lem7 4940  mulcanpi 5181  indpi 5188  prcdpq 5251  ltaddpr 5294  reclem2pr 5311  reclem3pr 5312  lediv2a 6042  nn1suc 6084  ser1add2i 6703  ser1addi 6704  2climnn 7305  2climnn0 7306  infcvgaux2i 7424  alephexp2 7798  strlem1 10458  uninqs 10730  infi1 10735  fiiu 10738  ficli 10756  imgfldref2 10768  ref3w 10772  xrletr2 10790  prj1 10809  set2elt 10827  fiiu2 10852  dupos1 10876  lteqtpos 10880  pospos 10882  tostos 10883  smgrpmgm 10912  smgrpass 10913  ismnd2 10928  mndid 10929  mndio 10930  mndass 10931  grpmnd 10933  on1el3 10962  bsi 10995  osneisi 11018  hmphre 11036  hmeogrp 11044  homcard 11045  top2ind 11050  filint 11075  fipfil2 11077  filintf 11081  filint2 11084  altretop 11144  iintlem1 11155  idfisf 11295  morsubc 11309  idsubfun 11312  dif1en 11833  neificl 11904  phtpcdm 12103

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

Copyright terms: Public domain