Theorem 2albii 1448

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

Step	Hyp	Ref	Expression
1		albii.1	. . 3 ⊢ (𝜑 ↔ 𝜓)
2	1	albii 1447	. 2 ⊢ (∀𝑦𝜑 ↔ ∀𝑦𝜓)
3	2	albii 1447	1 ⊢ (∀𝑥∀𝑦𝜑 ↔ ∀𝑥∀𝑦𝜓)

Syntax hints:   ↔ wb 104  ∀wal 1330

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 1424  ax-gen 1426

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  mor  2042  mo4f  2060  moanim  2074  2eu4  2093  ralcomf  2595  raliunxp  4688  cnvsym  4930  intasym  4931  intirr  4933  codir  4935  qfto  4936  dffun4  5142  dffun4f  5147  funcnveq  5194  fun11  5198  fununi  5199  mpo2eqb  5888  addnq0mo  7279  mulnq0mo  7280  addsrmo  7575  mulsrmo  7576