Theorem imdistand 447

Description: Distribution of implication with conjunction (deduction rule).

Hypothesis

Ref	Expression
imdistand.1	|- (ph -> (ps -> (ch -> th)))

Assertion

Ref	Expression
imdistand	|- (ph -> ((ps /\ ch) -> (ps /\ th)))

Proof of Theorem imdistand

Step	Hyp	Ref	Expression
1		imdistand.1	. 2 |- (ph -> (ps -> (ch -> th)))
2		imdistan 444	. 2 |- ((ps -> (ch -> th)) <-> ((ps /\ ch) -> (ps /\ th)))
3	1, 2	sylib 198	1 |- (ph -> ((ps /\ ch) -> (ps /\ th)))

Syntax hints:   -> wi 3   /\ wa 223

This theorem is referenced by:  pm5.3 448  fconstfv 3855  unblem1 4551  zorn2lem7 4804  cfub 4920  cflim 4921  prlem936b 5166  suppsr3 5236  supsrlem2 5238  uzss 6432  fsumsplit 7020  climaddc2 7119  cnsscnp 7769  cncnp 7775  ssbl 7852  lmle 7957  ocsh 9151

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

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

Copyright terms: Public domain