Theorem pm4.2i 149

Description: Principle of identity with antecedent.

Assertion

Ref	Expression
pm4.2i	⊢ (φ → (ψ ↔ ψ))

Proof of Theorem pm4.2i

Step	Hyp	Ref	Expression
1		pm4.2 148	. 2 ⊢ (ψ ↔ ψ)
2	1	a1i 7	1 ⊢ (φ → (ψ ↔ ψ))

Syntax hints:   → wi 2   ↔ wb 127

This theorem is referenced by:  sbidm 912  moeq3 1432  euxfr2 1435  reuxfr2 1579  soeq1 2141  so 2152  weinxp 2467  tz6.12-2 2845  rdgeq1 2972  rdgeq2 2973  aceq1 3552  aceq2 3554  axpowndlem4 3746  axpownd 3747  axinfndlem1 3751  axacndlem4 3756  ltsopr 3930  mulcant2 4209

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

This theorem depends on definitions:  df-bi 128

metamath.org