Theorem pm5.74da 589

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

Hypothesis

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

Assertion

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

Proof of Theorem pm5.74da

Step	Hyp	Ref	Expression
1		pm5.74da.1	. . 3 |- ((ph /\ ps) -> (ch <-> th))
2	1	ex 371	. 2 |- (ph -> (ps -> (ch <-> th)))
3	2	pm5.74d 588	1 |- (ph -> ((ps -> ch) <-> (ps -> th)))

Syntax hints:   -> wi 3   <-> wb 144   /\ wa 221

This theorem is referenced by:  ralbida 1703  sbc2iedv 2037  ordunisuc2 3198  dfom2 3220  suplem2pr 5316  uzindOLD 6379  cau2i 7116  metcnplem 8097  cncfmet 8116  dmdbr5ati 10631  limfilcf 11683  flimfcnp 11714  fcluscf 11724  fcluscomp 11733

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 145  df-an 223

Copyright terms: Public domain