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

Theorem imor 847
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 316 . . 3 (𝜑 ↔ ¬ ¬ 𝜑)
21imbi1i 351 . 2 ((𝜑𝜓) ↔ (¬ ¬ 𝜑𝜓))
3 df-or 842 . 2 ((¬ 𝜑𝜓) ↔ (¬ ¬ 𝜑𝜓))
42, 3bitr4i 279 1 ((𝜑𝜓) ↔ (¬ 𝜑𝜓))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 207  wo 841
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  df-or 842
This theorem is referenced by:  imori  848  imorri  849  pm4.62  850  pm4.78  928  pm4.52  978  dfifp4  1058  dfifp5  1059  dfifp7  1061  norasslem1  1521  rb-bijust  1741  rb-imdf  1742  rb-ax1  1744  nf2  1777  r19.30OLD  3336  relsnb  5668  soxp  7812  modom  8707  dffin7-2  9808  algcvgblem  15909  divgcdodd  16042  chrelat2i  30069  disjex  30270  disjexc  30271  meran1  33656  meran3  33658  bj-dfbi5  33804  bj-andnotim  33819  itg2addnclem2  34825  dvasin  34859  impor  35240  biimpor  35243  hlrelat2  36419  ifpim1  39712  ifpim2  39715  ifpidg  39735  ifpim23g  39739  ifpim123g  39744  ifpimimb  39748  ifpororb  39749  hbimpgVD  41115  stoweidlem14  42176  fvmptrabdm  43369  alimp-surprise  44809  eximp-surprise  44813
  Copyright terms: Public domain W3C validator