ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  ralrimdva GIF version

Theorem ralrimdva 2557
Description: Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 2-Feb-2008.)
Hypothesis
Ref Expression
ralrimdva.1 ((𝜑𝑥𝐴) → (𝜓𝜒))
Assertion
Ref Expression
ralrimdva (𝜑 → (𝜓 → ∀𝑥𝐴 𝜒))
Distinct variable groups:   𝜑,𝑥   𝜓,𝑥
Allowed substitution hints:   𝜒(𝑥)   𝐴(𝑥)

Proof of Theorem ralrimdva
StepHypRef Expression
1 ralrimdva.1 . . . 4 ((𝜑𝑥𝐴) → (𝜓𝜒))
21ex 115 . . 3 (𝜑 → (𝑥𝐴 → (𝜓𝜒)))
32com23 78 . 2 (𝜑 → (𝜓 → (𝑥𝐴𝜒)))
43ralrimdv 2556 1 (𝜑 → (𝜓 → ∀𝑥𝐴 𝜒))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 104  wcel 2148  wral 2455
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1447  ax-gen 1449  ax-4 1510  ax-17 1526
This theorem depends on definitions:  df-bi 117  df-nf 1461  df-ral 2460
This theorem is referenced by:  ralxfrd  4463  isoselem  5821  isosolem  5825  findcard  6888  nnsub  8958  supinfneg  9595  infsupneg  9596  ublbneg  9613  expnlbnd2  10646  cau3lem  11123  climshftlemg  11310  subcn2  11319  serf0  11360  sqrt2irr  12162  pclemub  12287  prmpwdvds  12353  grpinveu  12911  dfgrp3mlem  12968  issubg4m  13053  tgcn  13711  tgcnp  13712  lmconst  13719  cnntr  13728  lmss  13749  txdis  13780  txlm  13782  blbas  13936  metss  13997  metcnp3  14014  iswomni0  14802
  Copyright terms: Public domain W3C validator