ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  ralimdv Unicode 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  |-  ( ph  ->  ( ps  ->  ch ) )
Assertion
Ref Expression
ralimdv  |-  ( ph  ->  ( A. x  e.  A  ps  ->  A. x  e.  A  ch )
)
Distinct variable group:    ph, x
Allowed substitution hints:    ps( x)    ch( x)    A( x)

Proof of Theorem ralimdv
StepHypRef Expression
1 ralimdv.1 . . 3  |-  ( ph  ->  ( ps  ->  ch ) )
21adantr 276 . 2  |-  ( (
ph  /\  x  e.  A )  ->  ( ps  ->  ch ) )
32ralimdva 2544 1  |-  ( ph  ->  ( A. x  e.  A  ps  ->  A. x  e.  A  ch )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 2148   A.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  4298  sess1  4337  sess2  4338  riinint  4888  dffo4  5664  dffo5  5665  isoini2  5819  rdgivallem  6381  iinerm  6606  xpf1o  6843  exmidontriimlem3  7221  exmidontriim  7223  resqrexlemgt0  11028  cau3lem  11122  caubnd2  11125  climshftlemg  11309  climcau  11354  climcaucn  11358  serf0  11359  modfsummodlemstep  11464  bezoutlemmain  11998  ctinf  12430  strsetsid  12494  imasaddfnlemg  12734  fiinbas  13485  baspartn  13486  lmtopcnp  13686  rescncf  14004  limcresi  14071
  Copyright terms: Public domain W3C validator