Theorem hbbi 1008

Description: If x is not free in ph and ps, it is not free in (ph <-> ps).

Hypotheses

Ref	Expression
hb.1	|- (ph -> A.xph)
hb.2	|- (ps -> A.xps)

Assertion

Ref	Expression
hbbi	|- ((ph <-> ps) -> A.x(ph <-> ps))

Proof of Theorem hbbi

Step	Hyp	Ref	Expression
1		hb.1	. . . 4 |- (ph -> A.xph)
2		hb.2	. . . 4 |- (ps -> A.xps)
3	1, 2	hbim 1005	. . 3 |- ((ph -> ps) -> A.x(ph -> ps))
4	2, 1	hbim 1005	. . 3 |- ((ps -> ph) -> A.x(ps -> ph))
5	3, 4	hban 1007	. 2 |- (((ph -> ps) /\ (ps -> ph)) -> A.x((ph -> ps) /\ (ps -> ph)))
6		bi 514	. 2 |- ((ph <-> ps) <-> ((ph -> ps) /\ (ps -> ph)))
7	6	albii 997	. 2 |- (A.x(ph <-> ps) <-> A.x((ph -> ps) /\ (ps -> ph)))
8	5, 6, 7	3imtr4 219	1 |- ((ph <-> ps) -> A.x(ph <-> ps))

Syntax hints:   -> wi 3   <-> wb 146   /\ wa 223  A.wal 952

This theorem is referenced by:  euf 1382  sb8eu 1388  bm1.1 1460  cleqf 1557  hbeq 1562  ceqsexg 1883  elabgt 1891  elabf 1892  elabgf 1894  moi2 1920  moi 1921  sbhypf 1935  sbhyp 1936  sbcel1gv 1976  sbcel2gv 1977  sbcbrg 2657  axrep1 2689  axrep3 2691  axrep4 2692  copsex2g 2788  opabsb 2810  ralxpf 3215  cnvopab 3437  fvopab5 3784  hbiso 3883  zfcndrep 4946  nn1suc 5895  uzindOLD 6164

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

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

Copyright terms: Public domain