Theorem 2albii 1347

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

Syntax hints:   <-> wb 163  A.wal 1296

This theorem is referenced by:  hbsb4tOLD 1622  mo 1787  mo4f 1798  2mo 1851  2mos 1852  2eu4 1856  2eu6 1858  ralcom 2242  weinxp 4059  cnvsym 4304  intasym 4306  intasymOLD 4307  asymrefOLD 4309  intirr 4312  dffun4 4433  fun11 4480  fununi 4481  aceq0 5892  zfac 5907  zfcndac 6123  bnj142 12474  bnj869 12797  bnj979 12863  bnj582 13295  axacprim 13791  dfon2lem8 13856

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 1305  ax-4 1319  ax-5o 1321

This theorem depends on definitions:  df-bi 164  df-an 242

Copyright terms: Public domain