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

Theorem 2albii 1447
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 1446 . 2 (∀𝑦𝜑 ↔ ∀𝑦𝜓)
32albii 1446 1 (∀𝑥𝑦𝜑 ↔ ∀𝑥𝑦𝜓)
Colors of variables: wff set class
Syntax hints:  wb 104  wal 1329
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1423  ax-gen 1425
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  mor  2041  mo4f  2059  moanim  2073  2eu4  2092  ralcomf  2592  raliunxp  4680  cnvsym  4922  intasym  4923  intirr  4925  codir  4927  qfto  4928  dffun4  5134  dffun4f  5139  funcnveq  5186  fun11  5190  fununi  5191  mpo2eqb  5880  addnq0mo  7269  mulnq0mo  7270  addsrmo  7565  mulsrmo  7566
  Copyright terms: Public domain W3C validator