Theorem hband 1143

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

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 560	. 2 |- (ph -> ((ps /\ ch) -> (A.xps /\ A.xch)))
4		19.26 1099	. 2 |- (A.x(ps /\ ch) <-> (A.xps /\ A.xch))
5	3, 4	syl6ibr 211	1 |- (ph -> ((ps /\ ch) -> A.x(ps /\ ch)))

Syntax hints:   -> wi 3   /\ wa 221  A.wal 986

This theorem is referenced by:  hbsbc1gd 2023  hbsbcgd 2024  hbcsb1gd 2070  hbcsbgd 2071  dfid3 2890  axrepndlem1 5033  axrepndlem2 5034  axunndlem1 5036  axunnd 5037  axregndlem2 5044  axinfndlem1 5046  axinfnd 5047  axacndlem4 5051  axacndlem5 5052  axacnd 5053

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 995  ax-4 1005  ax-5o 1007

This theorem depends on definitions:  df-bi 145  df-an 223

Copyright terms: Public domain