Metamath Proof Explorer


Theorem bj-ceqsalt0

Description: The FOL content of ceqsalt . Lemma for bj-ceqsalt and bj-ceqsaltv . (Contributed by BJ, 26-Sep-2019) (Proof modification is discouraged.)

Ref Expression
Assertion bj-ceqsalt0 x ψ x θ φ ψ x θ x θ φ ψ

Proof

Step Hyp Ref Expression
1 simp3 x ψ x θ φ ψ x θ x θ
2 biimp φ ψ φ ψ
3 2 imim3i θ φ ψ θ φ θ ψ
4 3 al2imi x θ φ ψ x θ φ x θ ψ
5 4 3ad2ant2 x ψ x θ φ ψ x θ x θ φ x θ ψ
6 19.23t x ψ x θ ψ x θ ψ
7 6 3ad2ant1 x ψ x θ φ ψ x θ x θ ψ x θ ψ
8 5 7 sylibd x ψ x θ φ ψ x θ x θ φ x θ ψ
9 1 8 mpid x ψ x θ φ ψ x θ x θ φ ψ
10 biimpr φ ψ ψ φ
11 10 imim2i θ φ ψ θ ψ φ
12 11 com23 θ φ ψ ψ θ φ
13 12 alimi x θ φ ψ x ψ θ φ
14 13 3ad2ant2 x ψ x θ φ ψ x θ x ψ θ φ
15 19.21t x ψ x ψ θ φ ψ x θ φ
16 15 3ad2ant1 x ψ x θ φ ψ x θ x ψ θ φ ψ x θ φ
17 14 16 mpbid x ψ x θ φ ψ x θ ψ x θ φ
18 9 17 impbid x ψ x θ φ ψ x θ x θ φ ψ