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

Theorem 2albii 1405
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 1404 . 2 (∀𝑦𝜑 ↔ ∀𝑦𝜓)
32albii 1404 1 (∀𝑥𝑦𝜑 ↔ ∀𝑥𝑦𝜓)
Colors of variables: wff set class
Syntax hints:  wb 103  wal 1287
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 1381  ax-gen 1383
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  mor  1990  mo4f  2008  moanim  2022  2eu4  2041  ralcomf  2528  raliunxp  4577  cnvsym  4815  intasym  4816  intirr  4818  codir  4820  qfto  4821  dffun4  5026  dffun4f  5031  funcnveq  5077  fun11  5081  fununi  5082  mpt22eqb  5754  addnq0mo  7006  mulnq0mo  7007  addsrmo  7289  mulsrmo  7290
  Copyright terms: Public domain W3C validator