ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  3gencl Structured version   GIF version

Theorem 3gencl 2582
Description: Implicit substitution for class with embedded variable. (Contributed by NM, 17-May-1996.)
Hypotheses
Ref Expression
3gencl.1 (𝐷 𝑆x 𝑅 A = 𝐷)
3gencl.2 (𝐹 𝑆y 𝑅 B = 𝐹)
3gencl.3 (𝐺 𝑆z 𝑅 𝐶 = 𝐺)
3gencl.4 (A = 𝐷 → (φψ))
3gencl.5 (B = 𝐹 → (ψχ))
3gencl.6 (𝐶 = 𝐺 → (χθ))
3gencl.7 ((x 𝑅 y 𝑅 z 𝑅) → φ)
Assertion
Ref Expression
3gencl ((𝐷 𝑆 𝐹 𝑆 𝐺 𝑆) → θ)
Distinct variable groups:   x,y,z   y,𝐷,z   z,𝐹   x,𝑅,y   y,𝑆,z   ψ,x   χ,y   θ,z
Allowed substitution hints:   φ(x,y,z)   ψ(y,z)   χ(x,z)   θ(x,y)   A(x,y,z)   B(x,y,z)   𝐶(x,y,z)   𝐷(x)   𝑅(z)   𝑆(x)   𝐹(x,y)   𝐺(x,y,z)

Proof of Theorem 3gencl
StepHypRef Expression
1 3gencl.3 . . . . 5 (𝐺 𝑆z 𝑅 𝐶 = 𝐺)
2 df-rex 2306 . . . . 5 (z 𝑅 𝐶 = 𝐺z(z 𝑅 𝐶 = 𝐺))
31, 2bitri 173 . . . 4 (𝐺 𝑆z(z 𝑅 𝐶 = 𝐺))
4 3gencl.6 . . . . 5 (𝐶 = 𝐺 → (χθ))
54imbi2d 219 . . . 4 (𝐶 = 𝐺 → (((𝐷 𝑆 𝐹 𝑆) → χ) ↔ ((𝐷 𝑆 𝐹 𝑆) → θ)))
6 3gencl.1 . . . . . 6 (𝐷 𝑆x 𝑅 A = 𝐷)
7 3gencl.2 . . . . . 6 (𝐹 𝑆y 𝑅 B = 𝐹)
8 3gencl.4 . . . . . . 7 (A = 𝐷 → (φψ))
98imbi2d 219 . . . . . 6 (A = 𝐷 → ((z 𝑅φ) ↔ (z 𝑅ψ)))
10 3gencl.5 . . . . . . 7 (B = 𝐹 → (ψχ))
1110imbi2d 219 . . . . . 6 (B = 𝐹 → ((z 𝑅ψ) ↔ (z 𝑅χ)))
12 3gencl.7 . . . . . . 7 ((x 𝑅 y 𝑅 z 𝑅) → φ)
13123expia 1105 . . . . . 6 ((x 𝑅 y 𝑅) → (z 𝑅φ))
146, 7, 9, 11, 132gencl 2581 . . . . 5 ((𝐷 𝑆 𝐹 𝑆) → (z 𝑅χ))
1514com12 27 . . . 4 (z 𝑅 → ((𝐷 𝑆 𝐹 𝑆) → χ))
163, 5, 15gencl 2580 . . 3 (𝐺 𝑆 → ((𝐷 𝑆 𝐹 𝑆) → θ))
1716com12 27 . 2 ((𝐷 𝑆 𝐹 𝑆) → (𝐺 𝑆θ))
18173impia 1100 1 ((𝐷 𝑆 𝐹 𝑆 𝐺 𝑆) → θ)
Colors of variables: wff set class
Syntax hints:  wi 4   wa 97  wb 98   w3a 884   = wceq 1242  wex 1378   wcel 1390  wrex 2301
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-gen 1335  ax-ie2 1380  ax-17 1416
This theorem depends on definitions:  df-bi 110  df-3an 886  df-rex 2306
This theorem is referenced by:  axpre-ltwlin  6747  axpre-lttrn  6748  axpre-ltadd  6750  axpre-mulext  6752
  Copyright terms: Public domain W3C validator