Theorem pm5.32d 645

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

Hypothesis

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

Assertion

Ref	Expression
pm5.32d	|- (ph -> ((ps /\ ch) <-> (ps /\ th)))

Proof of Theorem pm5.32d

Step	Hyp	Ref	Expression
1		pm5.32d.1	. 2 |- (ph -> (ps -> (ch <-> th)))
2		pm5.32 642	. 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   /\ wa 223

This theorem is referenced by:  pm5.32rd 646  pm5.32da 647  cbval2 1311  cbvex2 1312  rabbirdv 2211  dfiun2g 2576  ordpwsuc 3056  ordsucun 3072  isoini 3885  rdglim2 3934  1idpr 5105  map2psrpr 5192  btwnz 6163  icounlem 6345  snunioolem 6347  divccncf 7215  efcltlem2 7247  metcnp 7826  occllem5 9093  rnbra 9953

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