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

Theorem rspc2va 3633
 Description: 2-variable restricted specialization, using implicit substitution. (Contributed by NM, 18-Jun-2014.)
Hypotheses
Ref Expression
rspc2v.1 (𝑥 = 𝐴 → (𝜑𝜒))
rspc2v.2 (𝑦 = 𝐵 → (𝜒𝜓))
Assertion
Ref Expression
rspc2va (((𝐴𝐶𝐵𝐷) ∧ ∀𝑥𝐶𝑦𝐷 𝜑) → 𝜓)
Distinct variable groups:   𝑥,𝑦,𝐴   𝑦,𝐵   𝑥,𝐶   𝑥,𝐷,𝑦   𝜒,𝑥   𝜓,𝑦
Allowed substitution hints:   𝜑(𝑥,𝑦)   𝜓(𝑥)   𝜒(𝑦)   𝐵(𝑥)   𝐶(𝑦)

Proof of Theorem rspc2va
StepHypRef Expression
1 rspc2v.1 . . 3 (𝑥 = 𝐴 → (𝜑𝜒))
2 rspc2v.2 . . 3 (𝑦 = 𝐵 → (𝜒𝜓))
31, 2rspc2v 3632 . 2 ((𝐴𝐶𝐵𝐷) → (∀𝑥𝐶𝑦𝐷 𝜑𝜓))
43imp 409 1 (((𝐴𝐶𝐵𝐷) ∧ ∀𝑥𝐶𝑦𝐷 𝜑) → 𝜓)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398   = wceq 1533   ∈ wcel 2110  ∀wral 3138 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 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-ext 2793 This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1777  df-cleq 2814  df-clel 2893  df-ral 3143 This theorem is referenced by:  swopo  5483  soisores  7079  soisoi  7080  isocnv  7082  isotr  7088  ovrspc2v  7181  caofrss  7441  caonncan  7446  wunpr  10130  injresinj  13157  seqcaopr2  13405  rlimcn2  14946  o1of2  14968  isprm6  16057  ssc2  17091  pospropd  17743  mhmpropd  17961  grpidssd  18174  grpinvssd  18175  dfgrp3lem  18196  isnsg3  18311  cyccom  18345  symgextf1  18548  efgredlemd  18869  efgredlem  18872  issrngd  19631  domneq0  20069  mplsubglem  20213  lindfind  20959  lindsind  20960  mdetunilem1  21220  mdetunilem3  21222  mdetunilem4  21223  mdetunilem9  21228  decpmatmulsumfsupp  21380  pm2mpf1  21406  pm2mpmhmlem1  21425  t0sep  21931  tsmsxplem2  22761  comet  23122  nrmmetd  23183  tngngp  23262  reconnlem2  23434  iscmet3lem1  23893  iscmet3lem2  23894  dchrisumlem1  26064  pntpbnd1  26161  tgjustc1  26260  tgjustc2  26261  iscgrglt  26299  motcgr  26321  perpneq  26499  foot  26507  f1otrg  26656  axcontlem10  26758  frgr2wwlk1  28107  tleile  30648  orngmul  30876  lindsunlem  31020  mndpluscn  31169  unelros  31430  difelros  31431  inelsros  31437  diffiunisros  31438  cvxsconn  32490  elmrsubrn  32767  ghomco  35168  mzpcl34  39328  ntrk0kbimka  40389  isotone1  40398  isotone2  40399  nnfoctbdjlem  42738  isomuspgrlem2d  43997  mgmhmpropd  44053  rnghmmul  44172
 Copyright terms: Public domain W3C validator