Metamath Proof Explorer


Theorem rr-phpd

Description: Equivalent of php without negation. (Contributed by Rohan Ridenour, 3-Aug-2023)

Ref Expression
Hypotheses rr-phpd.1 ( 𝜑𝐴 ∈ ω )
rr-phpd.2 ( 𝜑𝐵𝐴 )
rr-phpd.3 ( 𝜑𝐴𝐵 )
Assertion rr-phpd ( 𝜑𝐴 = 𝐵 )

Proof

Step Hyp Ref Expression
1 rr-phpd.1 ( 𝜑𝐴 ∈ ω )
2 rr-phpd.2 ( 𝜑𝐵𝐴 )
3 rr-phpd.3 ( 𝜑𝐴𝐵 )
4 2 adantr ( ( 𝜑 ∧ ¬ 𝐴 = 𝐵 ) → 𝐵𝐴 )
5 simpr ( ( 𝜑 ∧ ¬ 𝐴 = 𝐵 ) → ¬ 𝐴 = 𝐵 )
6 5 neqcomd ( ( 𝜑 ∧ ¬ 𝐴 = 𝐵 ) → ¬ 𝐵 = 𝐴 )
7 dfpss2 ( 𝐵𝐴 ↔ ( 𝐵𝐴 ∧ ¬ 𝐵 = 𝐴 ) )
8 4 6 7 sylanbrc ( ( 𝜑 ∧ ¬ 𝐴 = 𝐵 ) → 𝐵𝐴 )
9 php ( ( 𝐴 ∈ ω ∧ 𝐵𝐴 ) → ¬ 𝐴𝐵 )
10 1 8 9 syl2an2r ( ( 𝜑 ∧ ¬ 𝐴 = 𝐵 ) → ¬ 𝐴𝐵 )
11 10 ex ( 𝜑 → ( ¬ 𝐴 = 𝐵 → ¬ 𝐴𝐵 ) )
12 3 11 mt4d ( 𝜑𝐴 = 𝐵 )