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 272
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 271 . 2 ((𝜑 → (𝜓𝜒)) ↔ ((𝜑𝜓) ↔ (𝜑𝜒)))
31, 2mpbi 231 1 ((𝜑𝜓) ↔ (𝜑𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207
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 208
This theorem is referenced by:  bitrd  280  imbi2i  337  bibi2d  344  ibib  369  ibibr  370  pm5.4  390  pm5.42  544  anclb  546  ancrb  548  pm5.3  573  cases2  1039  cador  1600  equsalvw  2001  ax13b  2030  sbcom3vv  2097  equsalv  2258  equsal  2430  2sb6rf  2489  2sb6rfOLD  2490  sbcom3  2541  moeu  2661  ralbiia  3161  dfdif3  4088  frinxp  5627  idrefALT  5966  dfom2  7571  dfacacn  9555  kmlem8  9571  kmlem13  9576  kmlem14  9577  axgroth2  10235  rabeqsnd  30191  bnj1171  32169  bnj1253  32186  filnetlem4  33626  wl-equsalvw  34659  elintima  39876  ichexmpl2  43509
  Copyright terms: Public domain W3C validator