Theorem pm5.32d 446

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 444	. 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 444	. 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  447  pm5.32da  448  pm5.32  449  anbi2d  460  cbvex2  1910  cores  5106  isoini  5785  mpoeq123  5897  genpassl  7461  genpassu  7462  fzind  9302  btwnz  9306  elfzm11  10022  isprm2  12045  isprm3  12046  modprminv  12177  modprminveq  12178