Theorem mobiiOLD 2632

Description: Obsolete version of mobii 2631 as of 24-Sep-2023. (Contributed by NM, 9-Mar-1995.) (Revised by Mario Carneiro, 17-Oct-2016.) (Proof modification is discouraged.) (New usage is discouraged.)

Hypothesis

Ref	Expression
mobii.1	⊢ (𝜓 ↔ 𝜒)

Assertion

Ref	Expression
mobiiOLD	⊢ (∃*𝑥𝜓 ↔ ∃*𝑥𝜒)

Proof of Theorem mobiiOLD

Step	Hyp	Ref	Expression
1		mobi 2630	. 2 ⊢ (∀𝑥(𝜓 ↔ 𝜒) → (∃*𝑥𝜓 ↔ ∃*𝑥𝜒))
2		mobii.1	. 2 ⊢ (𝜓 ↔ 𝜒)
3	1, 2	mpg 1798	1 ⊢ (∃*𝑥𝜓 ↔ ∃*𝑥𝜒)

Syntax hints:   ↔ wb 208  ∃*wmo 2620

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-mo 2622

This theorem is referenced by: (None)