HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version

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
StepHypRef Expression
1 imdistand.1 . 2 |- (ph -> (ps -> (ch -> th)))
2 imdistan 768 . 2 |- ((ps -> (ch -> th)) <-> ((ps /\ ch) -> (ps /\ th)))
31, 2sylib 242 1 |- (ph -> ((ps /\ ch) -> (ps /\ th)))
Colors of variables: wff set class
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