Theorem pm5.32d 639

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

Hypothesis

Ref	Expression
pm5.32d.1

Assertion

Ref	Expression
pm5.32d

Proof of Theorem pm5.32d

Step	Hyp	Ref	Expression
1		pm5.32d.1	. 2
2		pm5.32 636	. 2
3	1, 2	sylib 196	1

Syntax hints:  ->wi 4  <->wb 184  /\wa 369

This theorem is referenced by:  pm5.32rd  640  pm5.32da  641  anbi2d  703  cbvex2OLD  2029  raltpd  4153  cores  5515  isoini  6234  mpt2eq123  6356  ordpwsuc  6650  rdglim2  7117  fzind  10987  btwnz  10991  elfzm11  11778  isprm2  14225  isprm3  14226  modprminv  14326  modprminveq  14327  isrim  17382  elimifd  27421  funcnvmptOLD  27509  xrecex  27616  ordtconlem1  27906  indpi1  28035  dfres3  29188  dfrdg4  29600  ee7.2aOLD  29926  wl-ax11-lem8  30032  expdioph  30965  pm14.122b  31330  rexbidar  31355  isrngim  32710

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 185  df-an 371