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

Theorem pm5.74i 259
 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 258 . 2 ((𝜑 → (𝜓𝜒)) ↔ ((𝜑𝜓) ↔ (𝜑𝜒)))
31, 2mpbi 219 1 ((𝜑𝜓) ↔ (𝜑𝜒))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 195 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 196 This theorem is referenced by:  bitrd  267  imbi2i  325  bibi2d  331  ibib  356  ibibr  357  anclb  568  pm5.42  569  ancrb  571  cador  1538  equsalvw  1918  ax13b  1951  equsalhw  2109  equsal  2279  sbcom3  2399  2sb6rf  2440  ralbiia  2962  frinxp  5107  dfom2  6959  dfacacn  8846  kmlem8  8862  kmlem13  8867  kmlem14  8868  axgroth2  9526  bnj1171  30322  bnj1253  30339  filnetlem4  31546  bj-ssb1a  31821  bj-ssb1  31822  bj-ssbcom3lem  31839  bj-equsalv  31931  wl-sbcom3  32551  elintima  36964
 Copyright terms: Public domain W3C validator