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

Theorem 2albii 1357
Description: Inference adding 2 universal quantifiers to both sides of an equivalence. (Contributed by NM, 9-Mar-1997.)
Hypothesis
Ref Expression
albii.1 (φψ)
Assertion
Ref Expression
2albii (xyφxyψ)

Proof of Theorem 2albii
StepHypRef Expression
1 albii.1 . . 3 (φψ)
21albii 1356 . 2 (yφyψ)
32albii 1356 1 (xyφxyψ)
Colors of variables: wff set class
Syntax hints:  wb 98  wal 1240
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 1333  ax-gen 1335
This theorem depends on definitions:  df-bi 110
This theorem is referenced by:  mor  1939  mo4f  1957  moanim  1971  2eu4  1990  ralcomf  2465  raliunxp  4420  cnvsym  4651  intasym  4652  intirr  4654  codir  4656  qfto  4657  dffun4  4856  dffun4f  4861  funcnveq  4905  fun11  4909  fununi  4910  mpt22eqb  5552  addnq0mo  6430  mulnq0mo  6431  addsrmo  6671  mulsrmo  6672
  Copyright terms: Public domain W3C validator