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

Theorem vtocl2ga 3578
Description: Implicit substitution of 2 classes for 2 setvar variables. (Contributed by NM, 20-Aug-1995.) Avoid ax-10 2139 and ax-11 2155. (Revised by GG, 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 340 . . 3 (𝑦 = 𝐵 → ((𝐴𝐶𝜓) ↔ (𝐴𝐶𝜒)))
3 vtocl2ga.1 . . . . . 6 (𝑥 = 𝐴 → (𝜑𝜓))
43imbi2d 340 . . . . 5 (𝑥 = 𝐴 → ((𝑦𝐷𝜑) ↔ (𝑦𝐷𝜓)))
5 vtocl2ga.3 . . . . . 6 ((𝑥𝐶𝑦𝐷) → 𝜑)
65ex 412 . . . . 5 (𝑥𝐶 → (𝑦𝐷𝜑))
74, 6vtoclga 3577 . . . 4 (𝐴𝐶 → (𝑦𝐷𝜓))
87com12 32 . . 3 (𝑦𝐷 → (𝐴𝐶𝜓))
92, 8vtoclga 3577 . 2 (𝐵𝐷 → (𝐴𝐶𝜒))
109impcom 407 1 ((𝐴𝐶𝐵𝐷) → 𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395   = wceq 1537  wcel 2106
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706
This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814
This theorem is referenced by:  vtocl3ga  3583  vtocl4ga  3586  solin  5623  caovcan  7637  xpord2pred  8169  pwfseqlem2  10697  mulcanenq  10998  ltaddnq  11012  ltrnq  11017  genpv  11037  wrdind  14757  fsumrelem  15840  imasleval  17588  fullfunc  17960  fthfunc  17961  symggrplem  18910  pf1ind  22375  mretopd  23116  dvlip  26047  scvxcvx  27044  issubgoilem  31289  cnre2csqlem  33871
  Copyright terms: Public domain W3C validator