NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  idd GIF version

Theorem idd 21
Description: Principle of identity with antecedent. (Contributed by NM, 26-Nov-1995.)
Assertion
Ref Expression
idd (φ → (ψψ))

Proof of Theorem idd
StepHypRef Expression
1 id 19 . 2 (ψψ)
21a1i 10 1 (φ → (ψψ))
Colors of variables: wff setvar class
Syntax hints:  wi 4
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7
This theorem is referenced by:  imim1d  69  simprim  142  pm2.6  162  pm2.65  164  orel2  372  pm2.621  397  simpr  447  ancld  536  ancrd  537  anim12d  546  anim1d  547  anim2d  548  pm2.63  763  orim1d  812  orim2d  813  ecase2d  906  cad0  1400  merco2  1501  spnfw  1670  19.2OLD  1700  r19.36av  2759  r19.44av  2767  r19.45av  2768  eqsbc3r  3103  reuss  3536  funiunfv  5467
  Copyright terms: Public domain W3C validator