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

Theorem 2albii 1401
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 1400 . 2  |-  ( A. y ph  <->  A. y ps )
32albii 1400 1  |-  ( A. x A. y ph  <->  A. x A. y ps )
Colors of variables: wff set class
Syntax hints:    <-> wb 103   A.wal 1283
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1377  ax-gen 1379
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  mor  1984  mo4f  2002  moanim  2016  2eu4  2035  ralcomf  2516  raliunxp  4505  cnvsym  4738  intasym  4739  intirr  4741  codir  4743  qfto  4744  dffun4  4943  dffun4f  4948  funcnveq  4993  fun11  4997  fununi  4998  mpt22eqb  5641  addnq0mo  6699  mulnq0mo  6700  addsrmo  6982  mulsrmo  6983
  Copyright terms: Public domain W3C validator