Theorem hband 1109

Description: Deduction form of bound-variable hypothesis builder hban 1007.

Hypotheses

Ref	Expression
hband.1	|- (ph -> (ps -> A.xps))
hband.2	|- (ph -> (ch -> A.xch))

Assertion

Ref	Expression
hband	|- (ph -> ((ps /\ ch) -> A.x(ps /\ ch)))

Proof of Theorem hband

Step	Hyp	Ref	Expression
1		hband.1	. . 3 |- (ph -> (ps -> A.xps))
2		hband.2	. . 3 |- (ph -> (ch -> A.xch))
3	1, 2	anim12d 557	. 2 |- (ph -> ((ps /\ ch) -> (A.xps /\ A.xch)))
4		19.26 1065	. 2 |- (A.x(ps /\ ch) <-> (A.xps /\ A.xch))
5	3, 4	syl6ibr 213	1 |- (ph -> ((ps /\ ch) -> A.x(ps /\ ch)))

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

This theorem is referenced by:  hbsbc1gd 1979  hbsbcgd 1980  hbcsb1gd 2023  hbcsbgd 2024  dfid3 2831  axrepndlem1 4924  axrepndlem2 4925  axunndlem1 4927  axunnd 4928  axregndlem2 4935  axinfndlem1 4937  axinfnd 4938  axacndlem4 4942  axacndlem5 4943  axacnd 4944

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

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

Copyright terms: Public domain