Theorem idd 75

Description: Principle of identity with antecedent.

Assertion

Ref	Expression
idd	|- (ph -> (ps -> ps))

Proof of Theorem idd

Step	Hyp	Ref	Expression
1		id 73	. 2 |- (ps -> ps)
2	1	a1i 8	1 |- (ph -> (ps -> ps))

Syntax hints:   -> wi 3

This theorem is referenced by:  pm2.63 474  anim1d 619  anim2d 620  orim1d 625  orim2d 626  dedlemaOLD 838  r19.36av 2232  r19.44av 2240  r19.45av 2241  eqsbc3r 2507  reuss 2871  opthpr 3156  relop 4113  abfii4 5654  ordtypelem6 5689  en3lplem2 5757  rankxplim3 5825  ra4sbc2 5829  sbcim2g 5841  omsubel 5883  elnnz 7354  expeq0 7828  expord2 7849  0top 8905  opni3 9143  lmfexlem1 9234  grpnnncan2 9378  va1cnlem 9684  ipsubdir 9849  minveceu 9928  soxp 13950  merco2 14203  meran1 14235  clfsebs 14707  fincmpzer 14711  svs2 14829  hmphsyma 14882  bwt2 14960  dualalg 15131  fiss 15368  ordtypelem6OLD 15380  omsubelOLD 15392  ist1-3 15543  fdc1 15813  totbndbnd 15944  ringsubdi 16106  ringsubdir 16107  ax10ext 16364  idn2 16509  idn3 16510  trsspwALT2 16641  sspwtrALT 16644  sstrALT2 16659  lubid 16807

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

Copyright terms: Public domain