Theorem hbal 981

Description: If x is not free in ph, it is not free in A.yph.

Hypothesis

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

Assertion

Ref	Expression
hbal	|- (A.yph -> A.xA.yph)

Proof of Theorem hbal

Step	Hyp	Ref	Expression
1		hb.1	. . 3 |- (ph -> A.xph)
2	1	19.20i 968	. 2 |- (A.yph -> A.yA.xph)
3		ax-7 954	. 2 |- (A.yA.xph -> A.xA.yph)
4	2, 3	syl 10	1 |- (A.yph -> A.xA.yph)

Syntax hints:   -> wi 3  A.wal 950

This theorem is referenced by:  hbex 982  aaan 1095  sb8 1245  cbval2 1298  euf 1361  mo 1370  2mo 1424  2eu3 1428  bm1.1 1439  hbeq 1541  hbral 1662  ralcom2 1752  moi 1896  uniiunlem 2103  hbint 2511  axrep1 2662  axrep2 2663  axrep3 2664  axrep4 2665  onminex 2983  dmcosseq 3316  fnoprabg 3951  axrepndlem1 4867  axacndlem4 4885  axacnd 4887  zfcndrep 4889  zfcndinf 4893  nnwof 6342

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-mp 7  ax-4 951  ax-5 952  ax-7 954  ax-gen 955

Copyright terms: Public domain