Metamath Proof Explorer


Theorem bj-ceqsalt1

Description: The FOL content of ceqsalt . Lemma for bj-ceqsalt and bj-ceqsaltv . TODO: consider removing if it does not add anything to bj-ceqsalt0 . (Contributed by BJ, 26-Sep-2019) (Proof modification is discouraged.)

Ref Expression
Hypothesis bj-ceqsalt1.1 θxχ
Assertion bj-ceqsalt1 xψxχφψθxχφψ

Proof

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