Theorem pm4.2i 171

Description: Principle of identity with antecedent.

Assertion

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

Proof of Theorem pm4.2i

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 892  3anbi13d 893  3anbi23d 894  3anbi1d 895  3anbi2d 896  3anbi3d 897  ax11 1217  sbidm 1252  a16g 1274  ax11indalem 1366  ax11inda2ALT 1367  moeq3 1917  euxfr2 1922  soeq1 2848  reuxfr2 2898  weinxp 3228  tz6.12-2 3730  oprabval6g 4023  eloprabi 4108  aceq1 4709  aceq2 4711  axpowndlem4 4932  axpownd 4933  axinfndlem1 4937  axacndlem4 4942  ltsopr 5116  ishomb 10596

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