Theorem pm5.74d 583

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 581	. 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 584  imbi2d 610  imbi2 622  cbvald 1315  2mos 1441  rcla4dv 1869  rcla4edv 1870  oneqmini 3007  findsg 3147  tfindsg 3152  brecop 4290  dom2d 4385  indpi 5006  nn1suc 5887  uzindOLD 6156  nn0ind-raph 6162  cncfmet 7844  iscms2lem4 7926  mdbr2 10133  dmdbr2 10140  mdsl2 10157  mdsl2b 10158  rcla4devOLD 10331

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