Theorem 2albii 1041

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 1040	. 2 |- (A.yph <-> A.yps)
3	2	albii 1040	1 |- (A.xA.yph <-> A.xA.yps)

Syntax hints:   <-> wb 153  A.wal 995

This theorem is referenced by:  hbsb4t 1291  mo 1435  mo4f 1444  2mo 1490  2mos 1491  2eu4 1495  2eu6 1497  ralcom 1821  weinxp 3290  intasym 3495  asymref 3496  dffun4 3585  fun11 3619  fununi 3620  aceq0 4792  axac 4807  zfcndac 5036

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 1004  ax-4 1014  ax-5o 1016

This theorem depends on definitions:  df-bi 154  df-an 232

Copyright terms: Public domain