Theorem 2albii 1517

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 1516	. 2 ⊢ (∀𝑦𝜑 ↔ ∀𝑦𝜓)
3	2	albii 1516	1 ⊢ (∀𝑥∀𝑦𝜑 ↔ ∀𝑥∀𝑦𝜓)

Syntax hints:   ↔ wb 105  ∀wal 1393

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1493  ax-gen 1495

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  mor  2120  mo4f  2138  moanim  2152  2eu4  2171  ralcomf  2692  raliunxp  4862  cnvsym  5111  intasym  5112  intirr  5114  codir  5116  qfto  5117  dffun4  5328  dffun4f  5333  funcnveq  5383  fun11  5387  fununi  5388  mpo2eqb  6113  addnq0mo  7630  mulnq0mo  7631  addsrmo  7926  mulsrmo  7927