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

Theorem ralimdv 2558
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 2557 1 (𝜑 → (∀𝑥𝐴 𝜓 → ∀𝑥𝐴 𝜒))
Colors of variables: wff set class
Syntax hints:  wi 4  wcel 2160  wral 2468
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 1458  ax-gen 1460  ax-4 1521  ax-17 1537
This theorem depends on definitions:  df-bi 117  df-nf 1472  df-ral 2473
This theorem is referenced by:  poss  4316  sess1  4355  sess2  4356  riinint  4906  dffo4  5685  dffo5  5686  isoini2  5841  rdgivallem  6406  iinerm  6633  xpf1o  6872  exmidontriimlem3  7252  exmidontriim  7254  resqrexlemgt0  11061  cau3lem  11155  caubnd2  11158  climshftlemg  11342  climcau  11387  climcaucn  11391  serf0  11392  modfsummodlemstep  11497  bezoutlemmain  12031  ctinf  12481  strsetsid  12545  imasaddfnlemg  12791  islss4  13698  fiinbas  14006  baspartn  14007  lmtopcnp  14207  rescncf  14525  limcresi  14592
  Copyright terms: Public domain W3C validator