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

Theorem rspc2va 3307
 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 3306 . 2 ((𝐴𝐶𝐵𝐷) → (∀𝑥𝐶𝑦𝐷 𝜑𝜓))
43imp 445 1 (((𝐴𝐶𝐵𝐷) ∧ ∀𝑥𝐶𝑦𝐷 𝜑) → 𝜓)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 384   = wceq 1480   ∈ wcel 1987  ∀wral 2907 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601 This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ral 2912  df-v 3188 This theorem is referenced by:  swopo  5005  soisores  6531  soisoi  6532  isocnv  6534  isotr  6540  ovrspc2v  6626  off  6865  caofrss  6883  caonncan  6888  wunpr  9475  injresinj  12529  seqcaopr2  12777  rlimcn2  14255  o1of2  14277  isprm6  15350  ssc2  16403  pospropd  17055  mhmpropd  17262  grpidssd  17412  grpinvssd  17413  dfgrp3lem  17434  isnsg3  17549  symgextf1  17762  efgredlemd  18078  efgredlem  18081  issrngd  18782  domneq0  19216  mplsubglem  19353  lindfind  20074  lindsind  20075  mdetunilem1  20337  mdetunilem3  20339  mdetunilem4  20340  mdetunilem9  20345  decpmatmulsumfsupp  20497  pm2mpf1  20523  pm2mpmhmlem1  20542  t0sep  21038  tsmsxplem2  21867  comet  22228  nrmmetd  22289  tngngp  22368  reconnlem2  22538  iscmet3lem1  22997  iscmet3lem2  22998  dchrisumlem1  25078  pntpbnd1  25175  motcgr  25331  perpneq  25509  foot  25514  f1otrg  25651  axcontlem10  25753  frgr2wwlk1  27052  tleile  29446  orngmul  29588  mndpluscn  29754  unelros  30015  difelros  30016  inelsros  30022  diffiunisros  30023  cvxsconn  30933  elmrsubrn  31125  ghomco  33322  mzpcl34  36774  ntrk0kbimka  37819  isotone1  37828  isotone2  37829  nnfoctbdjlem  39979  mgmhmpropd  41073  rnghmmul  41188
 Copyright terms: Public domain W3C validator