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 262
Description: Distribution of implication over biconditional (inference form). (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 261 . 2 ((𝜑 → (𝜓𝜒)) ↔ ((𝜑𝜓) ↔ (𝜑𝜒)))
31, 2mpbi 221 1 ((𝜑𝜓) ↔ (𝜑𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197
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 198
This theorem is referenced by:  bitrd  270  imbi2i  327  bibi2d  333  ibib  358  ibibr  359  pm5.42  539  anclb  541  ancrb  543  cases2  1070  cador  1717  equsalvw  2101  ax13b  2132  equsalv  2273  equsalhwOLD  2300  equsal  2390  sbcom3  2502  2sb6rf  2544  moeu  2597  ralbiia  3126  dfdif3  3884  frinxp  5356  idrefALT  5693  dfom2  7267  dfacacn  9218  kmlem8  9234  kmlem13  9239  kmlem14  9240  axgroth2  9902  rabeqsnd  29794  bnj1171  31519  bnj1253  31536  filnetlem4  32822  bj-ssb1a  33072  bj-ssb1  33073  bj-ssbcom3lem  33089  elintima  38623
  Copyright terms: Public domain W3C validator