Theorem pm5.32d 447

Description: Distribution of implication over biconditional (deduction form). (Contributed by NM, 29-Oct-1996.) (Revised by NM, 31-Jan-2015.)

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	. . . 4 |- ( ph -> ( ps -> ( ch <-> th ) ) )
2		biimp 117	. . . 4 |- ( ( ch <-> th ) -> ( ch -> th ) )
3	1, 2	syl6 33	. . 3 |- ( ph -> ( ps -> ( ch -> th ) ) )
4	3	imdistand 445	. 2 |- ( ph -> ( ( ps /\ ch ) -> ( ps /\ th ) ) )
5		biimpr 129	. . . 4 |- ( ( ch <-> th ) -> ( th -> ch ) )
6	1, 5	syl6 33	. . 3 |- ( ph -> ( ps -> ( th -> ch ) ) )
7	6	imdistand 445	. 2 |- ( ph -> ( ( ps /\ th ) -> ( ps /\ ch ) ) )
8	4, 7	impbid 128	1 |- ( ph -> ( ( ps /\ ch ) <-> ( ps /\ th ) ) )

Syntax hints:   -> wi 4   /\ wa 103   <-> wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  pm5.32rd  448  pm5.32da  449  pm5.32  450  anbi2d  461  cbvex2  1915  cores  5114  isoini  5797  mpoeq123  5912  genpassl  7486  genpassu  7487  fzind  9327  btwnz  9331  elfzm11  10047  isprm2  12071  isprm3  12072  modprminv  12203  modprminveq  12204