Axiom ax-bd0 17010

Description: If two formulas are equivalent, then boundedness of one implies boundedness of the other. (Contributed by BJ, 3-Oct-2019.)

Hypothesis

Ref	Expression
ax-bd0.1	⊢ (𝜑 ↔ 𝜓)

Assertion

Ref	Expression
ax-bd0	⊢ (BOUNDED 𝜑 → BOUNDED 𝜓)

Detailed syntax breakdown of Axiom ax-bd0

Step	Hyp	Ref	Expression
1		wph	. . 3 wff 𝜑
2	1	wbd 17009	. 2 wff BOUNDED 𝜑
3		wps	. . 3 wff 𝜓
4	3	wbd 17009	. 2 wff BOUNDED 𝜓
5	2, 4	wi 4	1 wff (BOUNDED 𝜑 → BOUNDED 𝜓)

This axiom is used by:  bdeq  17020  bd0  17021