Theorem hband 1469

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

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

Syntax hints:   -> wi 3   /\ wa 240  A.wal 1296

This theorem is referenced by:  hbsbc1gd 2515  hbsbc1gdOLD 2516  hbsbcgd 2517  hbsbcgdOLD 2518  hbcsb1gd 2570  hbcsbgd 2571  dfid3 3587  axrepndlem1 6096  axrepndlem2 6097  axunndlem1 6099  axunnd 6100  axregndlem2 6107  axinfndlem1 6109  axinfnd 6110  axacndlem4 6114  axacndlem5 6115  axacnd 6116

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 1305  ax-4 1319  ax-5o 1321

This theorem depends on definitions:  df-bi 164  df-an 242

Copyright terms: Public domain