Theorem pm5.32d 671

Description: Distribution of implication over biconditional (deduction rule). (Contributed by NM, 29-Oct-1996.)

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 668	. 2 |- ( ( ps -> ( ch <-> th ) ) <-> ( ( ps /\ ch ) <-> ( ps /\ th ) ) )
3	1, 2	sylib 208	1 |- ( ph -> ( ( ps /\ ch ) <-> ( ps /\ th ) ) )

Syntax hints:   -> wi 4   <-> wb 196   /\ wa 384

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 197  df-an 386

This theorem is referenced by:  pm5.32rd  672  pm5.32da  673  anbi2d  740  raltpd  4315  dfres3  5403  cores  5638  isoini  6588  mpt2eq123  6714  ordpwsuc  7015  rdglim2  7528  fzind  11475  btwnz  11479  elfzm11  12411  isprm2  15395  isprm3  15396  modprminv  15504  modprminveq  15505  isrim  18733  elimifd  29362  funcnvmptOLD  29467  xrecex  29628  ordtconnlem1  29970  indpi1  30082  dfrdg4  32058  ee7.2aOLD  32460  wl-ax11-lem8  33369  expdioph  37590  pm14.122b  38624  rexbidar  38650  mapsnend  39391  isrngim  41904