ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  r19.26 Unicode version

Theorem r19.26 2441
Description: Theorem 19.26 of [Margaris] p. 90 with restricted quantifiers. (Contributed by NM, 28-Jan-1997.) (Proof shortened by Andrew Salmon, 30-May-2011.)
Assertion
Ref Expression
r19.26  |-  ( A. x  e.  A  ( ph  /\  ps )  <->  ( A. x  e.  A  ph  /\  A. x  e.  A  ps ) )

Proof of Theorem r19.26
StepHypRef Expression
1 simpl 102 . . . 4  |-  ( (
ph  /\  ps )  ->  ph )
21ralimi 2384 . . 3  |-  ( A. x  e.  A  ( ph  /\  ps )  ->  A. x  e.  A  ph )
3 simpr 103 . . . 4  |-  ( (
ph  /\  ps )  ->  ps )
43ralimi 2384 . . 3  |-  ( A. x  e.  A  ( ph  /\  ps )  ->  A. x  e.  A  ps )
52, 4jca 290 . 2  |-  ( A. x  e.  A  ( ph  /\  ps )  -> 
( A. x  e.  A  ph  /\  A. x  e.  A  ps ) )
6 pm3.2 126 . . . 4  |-  ( ph  ->  ( ps  ->  ( ph  /\  ps ) ) )
76ral2imi 2385 . . 3  |-  ( A. x  e.  A  ph  ->  ( A. x  e.  A  ps  ->  A. x  e.  A  ( ph  /\  ps )
) )
87imp 115 . 2  |-  ( ( A. x  e.  A  ph 
/\  A. x  e.  A  ps )  ->  A. x  e.  A  ( ph  /\ 
ps ) )
95, 8impbii 117 1  |-  ( A. x  e.  A  ( ph  /\  ps )  <->  ( A. x  e.  A  ph  /\  A. x  e.  A  ps ) )
Colors of variables: wff set class
Syntax hints:    /\ wa 97    <-> wb 98   A.wral 2306
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1336  ax-gen 1338
This theorem depends on definitions:  df-bi 110  df-ral 2311
This theorem is referenced by:  r19.26-2  2442  r19.26-3  2443  ralbiim  2447  r19.27av  2448  reu8  2737  ssrab  3018  r19.28m  3311  r19.27m  3316  2ralunsn  3569  iuneq2  3673  cnvpom  4860  funco  4940  fncnv  4965  funimaexglem  4982  fnres  5015  fnopabg  5022  mpteqb  5261  eqfnfv3  5267  caoftrn  5736  iinerm  6178  rexanuz  9587  recvguniq  9593  cau3lem  9710  sqrt2irr  9878  bj-indind  10056
  Copyright terms: Public domain W3C validator