MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  vtocl2ga Structured version   Visualization version   GIF version

Theorem vtocl2ga 3572
Description: Implicit substitution of 2 classes for 2 setvar variables. (Contributed by NM, 20-Aug-1995.) Avoid ax-10 2136 and ax-11 2151. (Revised by Gino Giotto, 20-Aug-2023.) (Proof shortened by Wolf Lammen, 23-Aug-2023.)
Hypotheses
Ref Expression
vtocl2ga.1 (𝑥 = 𝐴 → (𝜑𝜓))
vtocl2ga.2 (𝑦 = 𝐵 → (𝜓𝜒))
vtocl2ga.3 ((𝑥𝐶𝑦𝐷) → 𝜑)
Assertion
Ref Expression
vtocl2ga ((𝐴𝐶𝐵𝐷) → 𝜒)
Distinct variable groups:   𝑥,𝑦,𝐴   𝑦,𝐵   𝑥,𝐶,𝑦   𝑥,𝐷,𝑦   𝜓,𝑥   𝜒,𝑦
Allowed substitution hints:   𝜑(𝑥,𝑦)   𝜓(𝑦)   𝜒(𝑥)   𝐵(𝑥)

Proof of Theorem vtocl2ga
StepHypRef Expression
1 vtocl2ga.2 . . . 4 (𝑦 = 𝐵 → (𝜓𝜒))
21imbi2d 342 . . 3 (𝑦 = 𝐵 → ((𝐴𝐶𝜓) ↔ (𝐴𝐶𝜒)))
3 vtocl2ga.1 . . . . . 6 (𝑥 = 𝐴 → (𝜑𝜓))
43imbi2d 342 . . . . 5 (𝑥 = 𝐴 → ((𝑦𝐷𝜑) ↔ (𝑦𝐷𝜓)))
5 vtocl2ga.3 . . . . . 6 ((𝑥𝐶𝑦𝐷) → 𝜑)
65ex 413 . . . . 5 (𝑥𝐶 → (𝑦𝐷𝜑))
74, 6vtoclga 3571 . . . 4 (𝐴𝐶 → (𝑦𝐷𝜓))
87com12 32 . . 3 (𝑦𝐷 → (𝐴𝐶𝜓))
92, 8vtoclga 3571 . 2 (𝐵𝐷 → (𝐴𝐶𝜒))
109impcom 408 1 ((𝐴𝐶𝐵𝐷) → 𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207  wa 396   = wceq 1528  wcel 2105
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-12 2167  ax-ext 2790
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1772  df-nf 1776  df-cleq 2811  df-clel 2890
This theorem is referenced by:  solin  5491  caovcan  7341  pwfseqlem2  10069  mulcanenq  10370  ltaddnq  10384  ltrnq  10389  genpv  10409  wrdind  14072  fsumrelem  15150  imasleval  16802  fullfunc  17164  fthfunc  17165  symggrplem  18456  pf1ind  20446  mretopd  21628  dvlip  24517  scvxcvx  25490  issubgoilem  28964  cnre2csqlem  31052
  Copyright terms: Public domain W3C validator