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

Theorem 2albii 1481
Description: Inference adding 2 universal quantifiers to both sides of an equivalence. (Contributed by NM, 9-Mar-1997.)
Hypothesis
Ref Expression
albii.1  |-  ( ph  <->  ps )
Assertion
Ref Expression
2albii  |-  ( A. x A. y ph  <->  A. x A. y ps )

Proof of Theorem 2albii
StepHypRef Expression
1 albii.1 . . 3  |-  ( ph  <->  ps )
21albii 1480 . 2  |-  ( A. y ph  <->  A. y ps )
32albii 1480 1  |-  ( A. x A. y ph  <->  A. x A. y ps )
Colors of variables: wff set class
Syntax hints:    <-> wb 105   A.wal 1361
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 1457  ax-gen 1459
This theorem depends on definitions:  df-bi 117
This theorem is referenced by:  mor  2078  mo4f  2096  moanim  2110  2eu4  2129  ralcomf  2648  raliunxp  4780  cnvsym  5024  intasym  5025  intirr  5027  codir  5029  qfto  5030  dffun4  5239  dffun4f  5244  funcnveq  5291  fun11  5295  fununi  5296  mpo2eqb  5998  addnq0mo  7460  mulnq0mo  7461  addsrmo  7756  mulsrmo  7757
  Copyright terms: Public domain W3C validator