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

Theorem imor 842
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 307 . . 3 (𝜑 ↔ ¬ ¬ 𝜑)
21imbi1i 341 . 2 ((𝜑𝜓) ↔ (¬ ¬ 𝜑𝜓))
3 df-or 837 . 2 ((¬ 𝜑𝜓) ↔ (¬ ¬ 𝜑𝜓))
42, 3bitr4i 270 1 ((𝜑𝜓) ↔ (¬ 𝜑𝜓))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 198  wo 836
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 199  df-or 837
This theorem is referenced by:  imori  843  imorri  844  pm4.62  845  pm4.78  921  pm4.52  970  dfifp4  1050  dfifp5  1051  dfifp7  1053  rb-bijust  1793  rb-imdf  1794  rb-ax1  1796  nf2  1829  r19.30  3268  relsnb  5475  soxp  7573  modom  8451  dffin7-2  9557  algcvgblem  15700  divgcdodd  15830  chrelat2i  29800  disjex  29972  disjexc  29973  meran1  32997  meran3  32999  bj-dfbi5  33141  bj-andnotim  33156  itg2addnclem2  34092  dvasin  34126  impor  34509  biimpor  34512  hlrelat2  35562  ifpim1  38781  ifpim2  38784  ifpidg  38804  ifpim23g  38808  ifpim123g  38813  ifpimimb  38817  ifpororb  38818  hbimpgVD  40083  stoweidlem14  41168  fvmptrabdm  42344  alimp-surprise  43642  eximp-surprise  43646
  Copyright terms: Public domain W3C validator