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  1043  cador  1610  equsalvw  2010  ax13b  2039  sbcom3vv  2103  equsalv  2265  equsal  2428  2sb6rf  2486  sbcom3  2525  moeu  2643  ralbiia  3132  dfdif3  4042  csbie2df  4348  frinxp  5599  idrefALT  5941  dfom2  7565  dfacacn  9555  kmlem8  9571  kmlem13  9576  kmlem14  9577  axgroth2  10239  rabeqsnd  30281  bnj1171  32397  bnj1253  32414  filnetlem4  33857  wl-equsalvw  34962  lcmineqlem4  39339  elintima  40397  ichexmpl2  44030
 Copyright terms: Public domain W3C validator