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

Theorem vtocl2ga 3534
Description: Implicit substitution of 2 classes for 2 setvar variables. (Contributed by NM, 20-Aug-1995.) Avoid ax-10 2138 and ax-11 2155. (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 341 . . 3 (𝑦 = 𝐵 → ((𝐴𝐶𝜓) ↔ (𝐴𝐶𝜒)))
3 vtocl2ga.1 . . . . . 6 (𝑥 = 𝐴 → (𝜑𝜓))
43imbi2d 341 . . . . 5 (𝑥 = 𝐴 → ((𝑦𝐷𝜑) ↔ (𝑦𝐷𝜓)))
5 vtocl2ga.3 . . . . . 6 ((𝑥𝐶𝑦𝐷) → 𝜑)
65ex 414 . . . . 5 (𝑥𝐶 → (𝑦𝐷𝜑))
74, 6vtoclga 3533 . . . 4 (𝐴𝐶 → (𝑦𝐷𝜓))
87com12 32 . . 3 (𝑦𝐷 → (𝐴𝐶𝜓))
92, 8vtoclga 3533 . 2 (𝐵𝐷 → (𝐴𝐶𝜒))
109impcom 409 1 ((𝐴𝐶𝐵𝐷) → 𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 397   = wceq 1542  wcel 2107
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2709
This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2816
This theorem is referenced by:  solin  5569  caovcan  7553  xpord2pred  8070  pwfseqlem2  10554  mulcanenq  10855  ltaddnq  10869  ltrnq  10874  genpv  10894  wrdind  14568  fsumrelem  15652  imasleval  17383  fullfunc  17753  fthfunc  17754  symggrplem  18654  pf1ind  21673  mretopd  22395  dvlip  25309  scvxcvx  26287  issubgoilem  30031  cnre2csqlem  32295
  Copyright terms: Public domain W3C validator