Theorem pm4.2d 171

Description: Principle of identity with antecedent.

Assertion

Ref	Expression
pm4.2d	|- (ph -> (ps <-> ps))

Proof of Theorem pm4.2d

Step	Hyp	Ref	Expression
1		pm4.2 170	. 2 |- (ps <-> ps)
2	1	a1i 8	1 |- (ph -> (ps <-> ps))

Syntax hints:   -> wi 3   <-> wb 146

This theorem is referenced by:  3anbi12d 898  3anbi13d 899  3anbi23d 900  3anbi1d 901  3anbi2d 902  3anbi3d 903  ax11 1225  sbidm 1260  a16g 1282  ax11indalem 1374  ax11inda2ALT 1375  moeq3 1928  euxfr2 1933  soeq1 2867  reuxfr2 2917  weinxp 3247  tz6.12-2 3753  oprabval6g 4046  eloprabi 4132  aceq1 4741  aceq2 4743  axpowndlem4 4965  axpownd 4966  axinfndlem1 4970  axacndlem4 4975  ltsopr 5149

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

This theorem depends on definitions:  df-bi 147

Copyright terms: Public domain