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

Theorem 2albii 1376
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 (∀𝑥𝑦𝜑 ↔ ∀𝑥𝑦𝜓)

Proof of Theorem 2albii
StepHypRef Expression
1 albii.1 . . 3 (𝜑𝜓)
21albii 1375 . 2 (∀𝑦𝜑 ↔ ∀𝑦𝜓)
32albii 1375 1 (∀𝑥𝑦𝜑 ↔ ∀𝑥𝑦𝜓)
Colors of variables: wff set class
Syntax hints:  wb 102  wal 1257
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-5 1352  ax-gen 1354
This theorem depends on definitions:  df-bi 114
This theorem is referenced by:  mor  1958  mo4f  1976  moanim  1990  2eu4  2009  ralcomf  2488  raliunxp  4505  cnvsym  4736  intasym  4737  intirr  4739  codir  4741  qfto  4742  dffun4  4941  dffun4f  4946  funcnveq  4990  fun11  4994  fununi  4995  mpt22eqb  5638  addnq0mo  6603  mulnq0mo  6604  addsrmo  6886  mulsrmo  6887
  Copyright terms: Public domain W3C validator