Theorem pm5.74da 646

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 402	. 2 |- (ph -> (ps -> (ch <-> th)))
3	2	pm5.74d 645	1 |- (ph -> ((ps -> ch) <-> (ps -> th)))

Syntax hints:   -> wi 3   <-> wb 163   /\ wa 240

This theorem is referenced by:  ralbida 2117  sbc2iedv 2524  ordunisuc2 3926  dfom2 3951  suplem2pr 6314  uzindOLD 7420  cau2i 8165  metcnplem 9164  cncfmet 9183  dmdbr5ati 11994  tfrALTlem 13976  conttnf 14944  dualcat2 15133  limfilcf 15587  flimfcnp 15602  fcluscf 15612  fcluscomp 15621

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 164  df-an 242

Copyright terms: Public domain