Theorem 2albii 997

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

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

This theorem is referenced by:  hbsb4t 1244  mo 1386  mo4f 1395  2mo 1440  2mos 1441  2eu4 1445  2eu6 1447  ralcom 1766  weinxp 3223  intasym 3422  asymref 3423  asymrefOLD 3425  dffun4 3514  fun11 3548  fununi 3549  aceq0 4702  axac 4717  zfcndac 4943

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 960  ax-4 970  ax-5o 972

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

Copyright terms: Public domain