Theorem pm5.74d 247

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

Hypothesis

Ref	Expression
pm5.74d.1

Assertion

Ref	Expression
pm5.74d

Proof of Theorem pm5.74d

Step	Hyp	Ref	Expression
1		pm5.74d.1	. 2
2		pm5.74 244	. 2
3	1, 2	sylib 196	1

Syntax hints:  ->wi 4  <->wb 184

This theorem is referenced by:  imbi2d  316  imim21b  367  pm5.74da  687  cbval2  2027  dvelimdf  2077  sbied  2151  dfiin2g  4363  oneqmini  4934  tfindsg  6695  findsg  6727  brecop  7423  dom2lem  7575  indpi  9306  uzindOLD  10982  nn0ind-raph  10989  cncls2  19774  ismbl2  21938  voliunlem3  21962  mdbr2  27215  dmdbr2  27222  mdsl2i  27241  mdsl2bi  27242  sgn3da  28480  wl-dral1d  29984  wl-equsald  29992  ralbidar  31354  bj-cbval2v  34302  cvlsupr3  35069  cdleme32fva  36163  cdlemk33N  36635  cdlemk34  36636

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