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

Theorem pm5.74i 260
 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 259 . 2 ((𝜑 → (𝜓𝜒)) ↔ ((𝜑𝜓) ↔ (𝜑𝜒)))
31, 2mpbi 220 1 ((𝜑𝜓) ↔ (𝜑𝜒))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 196 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 197 This theorem is referenced by:  bitrd  268  imbi2i  325  bibi2d  331  ibib  356  ibibr  357  anclb  569  pm5.42  570  ancrb  572  cases2  1016  cador  1587  equsalvw  1977  ax13b  2006  equsalv  2146  equsalhw  2161  equsal  2327  sbcom3  2439  2sb6rf  2480  ralbiia  3008  frinxp  5218  dfom2  7109  dfacacn  9001  kmlem8  9017  kmlem13  9022  kmlem14  9023  axgroth2  9685  rabeqsnd  29468  bnj1171  31194  bnj1253  31211  filnetlem4  32501  bj-ssb1a  32757  bj-ssb1  32758  bj-ssbcom3lem  32775  wl-sbcom3  33502  elintima  38262
 Copyright terms: Public domain W3C validator