MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  imor Structured version   Visualization version   GIF version

Theorem imor 428
Description: Implication in terms of disjunction. Theorem *4.6 of [WhiteheadRussell] p. 120. (Contributed by NM, 3-Jan-1993.)
Assertion
Ref Expression
imor ((𝜑𝜓) ↔ (¬ 𝜑𝜓))

Proof of Theorem imor
StepHypRef Expression
1 notnotb 304 . . 3 (𝜑 ↔ ¬ ¬ 𝜑)
21imbi1i 339 . 2 ((𝜑𝜓) ↔ (¬ ¬ 𝜑𝜓))
3 df-or 385 . 2 ((¬ 𝜑𝜓) ↔ (¬ ¬ 𝜑𝜓))
42, 3bitr4i 267 1 ((𝜑𝜓) ↔ (¬ 𝜑𝜓))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wo 383
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  df-or 385
This theorem is referenced by:  imori  429  imorri  430  pm4.62  435  pm4.52  512  pm4.78  605  dfifp4  1015  dfifp5  1016  dfifp7  1018  rb-bijust  1671  rb-imdf  1672  rb-ax1  1674  nf2  1708  r19.30  3076  soxp  7250  modom  8121  dffin7-2  9180  algcvgblem  15233  divgcdodd  15365  chrelat2i  29112  disjex  29291  disjexc  29292  meran1  32105  meran3  32107  bj-dfbi5  32254  bj-andnotim  32268  itg2addnclem2  33133  dvasin  33167  impor  33551  biimpor  33554  hlrelat2  34208  ifpim1  37333  ifpim2  37336  ifpidg  37356  ifpim23g  37360  ifpim123g  37365  ifpimimb  37369  ifpororb  37370  hbimpgVD  38662  stoweidlem14  39568  alimp-surprise  41859  eximp-surprise  41863
  Copyright terms: Public domain W3C validator