Theorem hbbi 705

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 702	. . 3 |- ((ph -> ps) -> A.x(ph -> ps))
4	2, 1	hbim 702	. . 3 |- ((ps -> ph) -> A.x(ps -> ph))
5	3, 4	hban 704	. 2 |- (((ph -> ps) /\ (ps -> ph)) -> A.x((ph -> ps) /\ (ps -> ph)))
6		bi 396	. 2 |- ((ph <-> ps) <-> ((ph -> ps) /\ (ps -> ph)))
7	6	bial 695	. 2 |- (A.x(ph <-> ps) <-> A.x((ph -> ps) /\ (ps -> ph)))
8	5, 6, 7	3imtr4 192	1 |- ((ph <-> ps) -> A.x(ph <-> ps))

Syntax hints:   -> wi 2   <-> wb 127   /\ wa 196  A.wal 672

This theorem is referenced by:  euf 1011  sb8eu 1017  bm1.1 1088  cleqf 1167  hbeq 1171  ceqsexg 1411  elabf 1414  elabgf 1416  vsbcint 1438  sbcel1 1466  sbcel2 1467  axrep 1473  axrep2 1474  zfrep2 1475  copsex2g 1903  reuuni2 1956  opabsb 2114  opelopabg 2115  cnvopab 2632  hbiso 2930  zfcndrep 3760  nn1suc 4435  uzind 4603

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-gen 677

This theorem depends on definitions:  df-bi 128  df-an 198

metamath.org