Theorem 2albii 1000

Description: Inference adding 2 universal quantifiers to both sides of an equivalence.

Hypothesis

Ref	Expression
albii.1	|- (ph <-> ps)

Assertion

Ref	Expression
2albii	|- (A.xA.yph <-> A.xA.yps)

Proof of Theorem 2albii

Step	Hyp	Ref	Expression
1		albii.1	. . 3 |- (ph <-> ps)
2	1	albii 999	. 2 |- (A.yph <-> A.yps)
3	2	albii 999	1 |- (A.xA.yph <-> A.xA.yps)

Syntax hints:   <-> wb 146  A.wal 954

This theorem is referenced by:  hbsb4t 1249  mo 1393  mo4f 1402  2mo 1447  2mos 1448  2eu4 1452  2eu6 1454  ralcom 1774  weinxp 3233  intasym 3438  asymref 3439  dffun4 3528  fun11 3562  fununi 3563  aceq0 4730  axac 4745  zfcndac 4971

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 963  ax-4 973  ax-5o 975

This theorem depends on definitions:  df-bi 147  df-an 225

Copyright terms: Public domain