MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  pm5.74d Unicode version

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
StepHypRef Expression
1 pm5.74d.1 . 2
2 pm5.74 244 . 2
31, 2sylib 196 1
Colors of variables: wff setvar class
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
  Copyright terms: Public domain W3C validator