MPE Home 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  571  pm5.42  572  ancrb  574  cases2  1034  cador  1696  equsalvw  2086  ax13b  2115  equsalv  2255  equsalhw  2270  equsal  2436  sbcom3  2548  2sb6rf  2589  ralbiia  3117  dfdif3  3863  frinxp  5341  dfom2  7232  dfacacn  9155  kmlem8  9171  kmlem13  9176  kmlem14  9177  axgroth2  9839  rabeqsnd  29649  bnj1171  31375  bnj1253  31392  filnetlem4  32682  bj-ssb1a  32938  bj-ssb1  32939  bj-ssbcom3lem  32956  wl-sbcom3  33685  elintima  38447
  Copyright terms: Public domain W3C validator