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

Theorem pm5.74da 687
Description: Distribution of implication over biconditional (deduction rule). (Contributed by NM, 4-May-2007.)
Hypothesis
Ref Expression
pm5.74da.1
Assertion
Ref Expression
pm5.74da

Proof of Theorem pm5.74da
StepHypRef Expression
1 pm5.74da.1 . . 3
21ex 434 . 2
32pm5.74d 247 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184  /\wa 369
This theorem is referenced by:  ralbida  2890  ralbidva  2893  ralxpxfr2d  3224  elrab3t  3256  ordunisuc2  6679  dfom2  6702  pwfseqlem3  9059  uzindOLD  10982  lo1resb  13387  rlimresb  13388  o1resb  13389  fsumparts  13620  isprm3  14226  ramval  14526  islindf4  18873  cnntr  19776  fclsbas  20522  metcnp  21044  voliunlem3  21962  ellimc2  22281  limcflf  22285  mdegleb  22464  xrlimcnp  23298  dchrelbas3  23513  lmicom  24154  dmdbr5ati  27341  isarchi3  27731  cmpcref  27853  sscoid  29563  jm2.25  30941  fourierdlem87  31976  cdlemefrs29bpre0  36122  cdlemkid3N  36659  cdlemkid4  36660  hdmap1eulem  37551  hdmap1eulemOLDN  37552
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
  Copyright terms: Public domain W3C validator