New Foundations Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  NFE Home  >  Th. List  >  3gencl GIF version

Theorem 3gencl 2889
 Description: Implicit substitution for class with embedded variable. (Contributed by NM, 17-May-1996.)
Hypotheses
Ref Expression
3gencl.1 (D Sx R A = D)
3gencl.2 (F Sy R B = F)
3gencl.3 (G Sz R C = G)
3gencl.4 (A = D → (φψ))
3gencl.5 (B = F → (ψχ))
3gencl.6 (C = G → (χθ))
3gencl.7 ((x R y R z R) → φ)
Assertion
Ref Expression
3gencl ((D S F S G S) → θ)
Distinct variable groups:   x,y,z   y,D,z   z,F   x,R,y   y,S,z   ψ,x   χ,y   θ,z
Allowed substitution hints:   φ(x,y,z)   ψ(y,z)   χ(x,z)   θ(x,y)   A(x,y,z)   B(x,y,z)   C(x,y,z)   D(x)   R(z)   S(x)   F(x,y)   G(x,y,z)

Proof of Theorem 3gencl
StepHypRef Expression
1 3gencl.3 . . . . 5 (G Sz R C = G)
2 df-rex 2620 . . . . 5 (z R C = Gz(z R C = G))
31, 2bitri 240 . . . 4 (G Sz(z R C = G))
4 3gencl.6 . . . . 5 (C = G → (χθ))
54imbi2d 307 . . . 4 (C = G → (((D S F S) → χ) ↔ ((D S F S) → θ)))
6 3gencl.1 . . . . . 6 (D Sx R A = D)
7 3gencl.2 . . . . . 6 (F Sy R B = F)
8 3gencl.4 . . . . . . 7 (A = D → (φψ))
98imbi2d 307 . . . . . 6 (A = D → ((z Rφ) ↔ (z Rψ)))
10 3gencl.5 . . . . . . 7 (B = F → (ψχ))
1110imbi2d 307 . . . . . 6 (B = F → ((z Rψ) ↔ (z Rχ)))
12 3gencl.7 . . . . . . 7 ((x R y R z R) → φ)
13123expia 1153 . . . . . 6 ((x R y R) → (z Rφ))
146, 7, 9, 11, 132gencl 2888 . . . . 5 ((D S F S) → (z Rχ))
1514com12 27 . . . 4 (z R → ((D S F S) → χ))
163, 5, 15gencl 2887 . . 3 (G S → ((D S F S) → θ))
1716com12 27 . 2 ((D S F S) → (G Sθ))
18173impia 1148 1 ((D S F S G S) → θ)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 176   ∧ wa 358   ∧ w3a 934  ∃wex 1541   = wceq 1642   ∈ wcel 1710  ∃wrex 2615 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616 This theorem depends on definitions:  df-bi 177  df-an 360  df-3an 936  df-ex 1542  df-rex 2620 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator