Theorem pm2.43i 78

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 73	. 2 |- (ph -> ph)
2		pm2.43i.1	. 2 |- (ph -> (ph -> ps))
3	1, 2	mpd 29	1 |- (ph -> ps)

Syntax hints:   -> wi 3

This theorem is referenced by:  pm2.18 97  anidm 478  anidms 480  anabsi5 553  ibi 652  3anidm12 1154  ee23 1276  hbequid 1313  equidqe 1314  ax4 1318  equid 1484  equidALT 1485  ax10 1501  hbae 1505  equid1 1646  ax11inda 1762  vtoclgaf 2350  vtoclgafOLD 2351  sbcth2 2514  elinti 3223  ssiun2s 3297  copsexg 3537  copsexgOLD 3538  tz7.7 3684  nsuceq0 3749  reuuni2f 3810  oprabvalig 4953  reiota2f 5109  tfrlem9 5127  tfrlem11 5129  omclOLD 5217  oeclOLD 5219  odi 5258  nnmclOLD 5284  nneclOLD 5286  sbth 5520  ee1111 5834  zorn2lem6 5955  zorn2lem7 5956  mulcanpi 6179  indpi 6186  prcdpq 6249  ltaddpr 6292  reclem2pr 6309  reclem3pr 6310  lediv2a 7080  nn1suc 7122  ser1add2i 7751  ser1addi 7752  2climnn 8362  2climnn0 8363  infcvgaux2i 8481  alephexp2 8855  dif1enOLD 10173  fiiu2 10220  filint 10269  fipfil2 10272  filintf 10274  clmgm 10368  smgrpmgm 10382  smgrpass 10383  ismnd2 10392  grpmnd 10393  on1el3 10412  strlem1 11822  bnj981 13356  bnj1129 13425  bnj1148 13434  bnj1152 13437  nn0seqcvgd 13659  ndvdssub 13710  algrp1lem 13741  dfon2lem3 13851  tbw-bijust 14165  tbw-negdf 14166  consym1 14244  unisym1 14247  uninqs 14340  infi1 14343  fiiu 14344  ficli 14353  imgfldref2 14368  ref4w 14370  prj1 14395  set2elt 14408  inttrp 14437  onsubcum 14442  celsor 14443  resrelfld 14448  eqfnung2 14459  surjsec 14462  inpreima2 14468  mapmapmap 14486  injsurinj 14487  elixp2a 14493  elixp2b 14494  npincppr 14501  repfuntw 14502  cbicplem 14508  prjnpl 14510  prjmapcp2 14515  iscst2 14520  preodom2 14567  preoran2 14571  preotr2 14576  altprs2 14577  int2pre 14578  dupos1 14586  sege 14595  supdef 14604  mxlmnl2 14612  defse3 14614  dutos1 14626  istoset2 14628  nfwpr4c 14630  pospos 14635  tostos 14637  dffprod 14670  iscomb 14690  clfsebs 14707  clfsebs2 14710  mndid 14718  mndio 14719  mndass 14720  mgmrddd 14727  ltlga 14729  fnopabco2b 14734  grpdivone 14736  grpdivfo 14737  fprodneg 14741  zerdivemp1 14785  svs2 14829  bsi 14845  inttop4 14865  osneisi 14875  hmphre 14884  hmeogrp 14892  homcard 14893  top2ind 14897  prtoptop 14919  filint2 14923  limfilnei 14943  conttnf 14944  iscnp3 14946  topgrpbs 14974  altretop 14997  cntrsetlem 14999  iintlem1 15010  xrletr2 15018  lteqtpos 15024  mamb 15030  lvsovso 15038  lvsovso3 15040  supnuf 15041  supbrr 15048  dualded 15132  dualcat2 15133  idfisf 15189  morsubc 15203  idsubfun 15206  tarax1 15216  tarax2 15217  tarax3 15218  elincin 15220  tarax3a 15222  tarax3c 15224  cptarc 15242  sexptrt 15243  tarsuc2 15245  inttaror 15277  oprabval2a 15707  neificl 15841  phtpcdm 16061  zerdivemp1x 16108  risci 16141  e222 16526  e111 16564  e333 16601  clatlem 16889

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

Copyright terms: Public domain