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

Theorem imor 426
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 302 . . 3 (𝜑 ↔ ¬ ¬ 𝜑)
21imbi1i 337 . 2 ((𝜑𝜓) ↔ (¬ ¬ 𝜑𝜓))
3 df-or 383 . 2 ((¬ 𝜑𝜓) ↔ (¬ ¬ 𝜑𝜓))
42, 3bitr4i 265 1 ((𝜑𝜓) ↔ (¬ 𝜑𝜓))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 194  wo 381
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 195  df-or 383
This theorem is referenced by:  imori  427  imorri  428  pm4.62  433  pm4.52  510  pm4.78  603  dfifp4  1009  dfifp5  1010  dfifp7  1012  rb-bijust  1664  rb-imdf  1665  rb-ax1  1667  nf2  1701  r19.30  3058  soxp  7150  modom  8019  dffin7-2  9076  algcvgblem  15070  divgcdodd  15202  chrelat2i  28410  disjex  28589  disjexc  28590  meran1  31382  meran3  31384  bj-dfbi5  31531  bj-andnotim  31548  bj-nf2  31568  itg2addnclem2  32431  dvasin  32465  impor  32849  biimpor  32852  hlrelat2  33506  ifpim1  36631  ifpim2  36634  ifpidg  36654  ifpim23g  36658  ifpim123g  36663  ifpimimb  36667  ifpororb  36668  hbimpgVD  37961  stoweidlem14  38707  alimp-surprise  42294  eximp-surprise  42298
  Copyright terms: Public domain W3C validator