Theorem pm5.74d 585

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 583	. 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 586  imbi2d 612  imbi2 624  cbvald 1320  2mos 1448  rcla4dv 1878  rcla4edv 1879  oneqmini 3017  findsg 3157  tfindsg 3162  brecop 4306  dom2d 4404  indpi 5034  nn1suc 5939  uzindOLD 6208  nn0ind-raph 6214  cncfmet 7905  iscms2lem4 7992  mdbr2 10223  dmdbr2 10230  mdsl2 10249  mdsl2b 10250  rcla4devOLD 10431

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