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

Theorem ralimdv 2545
Description: Deduction quantifying both antecedent and consequent, based on Theorem 19.20 of [Margaris] p. 90. (Contributed by NM, 8-Oct-2003.)
Hypothesis
Ref Expression
ralimdv.1 (𝜑 → (𝜓𝜒))
Assertion
Ref Expression
ralimdv (𝜑 → (∀𝑥𝐴 𝜓 → ∀𝑥𝐴 𝜒))
Distinct variable group:   𝜑,𝑥
Allowed substitution hints:   𝜓(𝑥)   𝜒(𝑥)   𝐴(𝑥)

Proof of Theorem ralimdv
StepHypRef Expression
1 ralimdv.1 . . 3 (𝜑 → (𝜓𝜒))
21adantr 276 . 2 ((𝜑𝑥𝐴) → (𝜓𝜒))
32ralimdva 2544 1 (𝜑 → (∀𝑥𝐴 𝜓 → ∀𝑥𝐴 𝜒))
Colors of variables: wff set class
Syntax hints:  wi 4  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:  poss  4300  sess1  4339  sess2  4340  riinint  4890  dffo4  5666  dffo5  5667  isoini2  5822  rdgivallem  6384  iinerm  6609  xpf1o  6846  exmidontriimlem3  7224  exmidontriim  7226  resqrexlemgt0  11031  cau3lem  11125  caubnd2  11128  climshftlemg  11312  climcau  11357  climcaucn  11361  serf0  11362  modfsummodlemstep  11467  bezoutlemmain  12001  ctinf  12433  strsetsid  12497  imasaddfnlemg  12740  islss4  13474  fiinbas  13588  baspartn  13589  lmtopcnp  13789  rescncf  14107  limcresi  14174
  Copyright terms: Public domain W3C validator