Theorem pm5.74d 587

Description: Distribution of implication over biconditional (deduction rule).

Hypothesis

Ref	Expression
pm5.74d.1	|- (ph -> (ps -> (ch <-> th)))

Assertion

Ref	Expression
pm5.74d	|- (ph -> ((ps -> ch) <-> (ps -> th)))

Proof of Theorem pm5.74d

Step	Hyp	Ref	Expression
1		pm5.74d.1	. 2 |- (ph -> (ps -> (ch <-> th)))
2		pm5.74 585	. 2 |- ((ps -> (ch <-> th)) <-> ((ps -> ch) <-> (ps -> th)))
3	1, 2	sylib 198	1 |- (ph -> ((ps -> ch) <-> (ps -> th)))

Syntax hints:   -> wi 3   <-> wb 146

This theorem is referenced by:  pm5.74da 588  imbi2d 614  imbi2 626  cbvald 1322  2mos 1451  rcla4dv 1881  rcla4edv 1882  oneqmini 3023  findsg 3163  tfindsg 3168  brecop 4312  dom2d 4410  indpi 5046  nn1suc 5941  uzindOLD 6210  nn0ind-raph 6216  cncfmet 7902  iscms2lem4 7989  mdbr2 10218  dmdbr2 10225  mdsl2 10244  mdsl2b 10245  rcla4devOLD 10426

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