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 274
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 273 . 2 ((𝜑 → (𝜓𝜒)) ↔ ((𝜑𝜓) ↔ (𝜑𝜒)))
31, 2mpbi 233 1 ((𝜑𝜓) ↔ (𝜑𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209
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 210
This theorem is referenced by:  bitrd  282  imbi2i  339  bibi2d  346  ibib  371  ibibr  372  pm5.4  393  pm5.42  547  anclb  549  ancrb  551  pm5.3  576  cases2  1048  cador  1615  equsalvw  2012  ax13b  2040  sbcom3vv  2102  equsalv  2264  equsal  2416  2sb6rf  2472  sbcom3  2509  moeu  2582  ralbiia  3087  ceqsalv  3443  ceqsralv  3445  clel2g  3566  clel4g  3571  elabg  3585  dfdif3  4029  csbie2df  4355  ralsng  4589  frinxp  5631  idrefALT  5978  dfom2  7646  dfacacn  9755  kmlem8  9771  kmlem13  9776  kmlem14  9777  axgroth2  10439  rabeqsnd  30567  bnj1171  32693  bnj1253  32710  filnetlem4  34307  wl-equsalvw  35434  lcmineqlem4  39774  dvrelog2b  39807  elintima  40938  ichexmpl2  44595
  Copyright terms: Public domain W3C validator