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 3849  unblem1 4540  zorn2lem7 4794  cfub 4908  cflim 4909  prlem936b 5154  suppsr3 5224  supsrlem2 5226  uzss 6431  fsumsplit 7020  climaddc2 7119  cnsscnp 7772  cncnp 7778  ssbl 7855  lmle 7960  ocsh 9156

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