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

Theorem pm5.74i 245
Description: Distribution of implication over biconditional (inference rule). (Contributed by NM, 1-Aug-1994.)
Hypothesis
Ref Expression
pm5.74i.1
Assertion
Ref Expression
pm5.74i

Proof of Theorem pm5.74i
StepHypRef Expression
1 pm5.74i.1 . 2
2 pm5.74 244 . 2
31, 2mpbi 208 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184
This theorem is referenced by:  bitrd  253  imbi2i  312  bibi2d  318  ibib  342  ibibr  343  anclb  547  pm5.42  548  ancrb  550  cador  1458  ax13b  1805  equsalhw  1945  equsal  2036  sbcom3  2153  2sb6rf  2196  ralbiia  2887  frinxp  5070  dfom2  6702  dfacacn  8542  kmlem8  8558  kmlem13  8563  kmlem14  8564  axgroth2  9224  uzindOLD  10982  wl-sbcom3  30035  filnetlem4  30199  bnj1171  34056  bnj1253  34073  bj-equsalv  34309  bj-equsalvv  34310  elintima  37765
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