Theorem imdistand 445

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 442	. 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 446  fconstfv 3840  unblem1 4523  zorn2lem7 4774  cfub 4888  cflim 4889  prlem936b 5134  suppsr3 5204  supsrlem2 5206  uzss 6371  fsumsplit 6966  climaddc2 7063  cnsscnp 7722  cncnp 7728  ssbl 7807  lmle 7911  ocsh 9095

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