Theorem hbbi 1010

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 1007	. . 3 |- ((ph -> ps) -> A.x(ph -> ps))
4	2, 1	hbim 1007	. . 3 |- ((ps -> ph) -> A.x(ps -> ph))
5	3, 4	hban 1009	. 2 |- (((ph -> ps) /\ (ps -> ph)) -> A.x((ph -> ps) /\ (ps -> ph)))
6		dfbi2 514	. 2 |- ((ph <-> ps) <-> ((ph -> ps) /\ (ps -> ph)))
7	6	albii 999	. 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 954

This theorem is referenced by:  euf 1384  sb8eu 1390  bm1.1 1462  cleqf 1560  hbeq 1565  ceqsexg 1887  elabgt 1895  elabf 1896  elabgf 1898  moi2 1924  moi 1925  sbhypf 1939  sbhyp 1940  sbcel1gv 1980  sbcel2gv 1981  sbcbrg 2662  axrep1 2694  axrep3 2696  axrep4 2697  copsex2g 2793  opabsb 2815  ralxpf 3220  cnvopab 3445  fvopab5 3793  hbiso 3892  zfcndrep 4966  nn1suc 5939  uzindOLD 6208

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  ax-6o 978

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

Copyright terms: Public domain