Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  djuf1olem Unicode version

Theorem djuf1olem 6938
 Description: Lemma for djulf1o 6943 and djurf1o 6944. (Contributed by BJ and Jim Kingdon, 4-Jul-2022.)
Hypotheses
Ref Expression
djuf1olem.1
djuf1olem.2
Assertion
Ref Expression
djuf1olem
Distinct variable groups:   ,   ,
Allowed substitution hint:   ()

Proof of Theorem djuf1olem
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 djuf1olem.2 . . 3
2 djuf1olem.1 . . . . . 6
32snid 3556 . . . . 5
4 opelxpi 4571 . . . . 5
53, 4mpan 420 . . . 4
7 xp2nd 6064 . . . 4
9 1st2nd2 6073 . . . . . . . 8
10 xp1st 6063 . . . . . . . . . 10
11 elsni 3545 . . . . . . . . . 10
1210, 11syl 14 . . . . . . . . 9
1312opeq1d 3711 . . . . . . . 8
149, 13eqtrd 2172 . . . . . . 7
1514eqeq2d 2151 . . . . . 6
16 eqcom 2141 . . . . . 6
17 eqid 2139 . . . . . . 7
18 vex 2689 . . . . . . . 8
192, 18opth 4159 . . . . . . 7
2017, 19mpbiran 924 . . . . . 6
2115, 16, 203bitr3g 221 . . . . 5
2221bicomd 140 . . . 4