Theorem imdistand 772

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 768	. 2 |- ((ps -> (ch -> th)) <-> ((ps /\ ch) -> (ps /\ th)))
3	1, 2	sylib 242	1 |- (ph -> ((ps /\ ch) -> (ps /\ th)))

Syntax hints:   -> wi 3   /\ wa 337

This theorem is referenced by:  fconstfv 4917  unblem1 5852  cfub 6268  cflim 6269  zorn2lem7 6367  prlem936b 6672  suppsr3 6742  supsrlem2 6744  fzind 7768  uzss 7947  lbzbi 7996  fsumsplit 8676  climaddc2 8775  cnsscnp 9915  cncnp 9921  ssbl 9998  lmle 10104  ocsh 11623  predpo 14537  tz6.26 14558  fcluscf 16436  flimfcls 16437  imdistanda 16476  totbndbnd 16768  heiborlem28 16806  rrncms 16843  ispridl2 17010  ispridlc 17042

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 220  df-an 339

Copyright terms: Public domain