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

Theorem imor 850
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 318 . . 3 (𝜑 ↔ ¬ ¬ 𝜑)
21imbi1i 353 . 2 ((𝜑𝜓) ↔ (¬ ¬ 𝜑𝜓))
3 df-or 845 . 2 ((¬ 𝜑𝜓) ↔ (¬ ¬ 𝜑𝜓))
42, 3bitr4i 281 1 ((𝜑𝜓) ↔ (¬ 𝜑𝜓))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 209  wo 844
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  df-or 845
This theorem is referenced by:  imori  851  imorri  852  pm4.62  853  pm4.78  932  pm4.52  982  dfifp4  1062  dfifp5  1063  dfifp7  1065  norasslem1  1531  rb-bijust  1751  rb-imdf  1752  rb-ax1  1754  nf2  1787  r19.30OLD  3331  relsnb  5663  soxp  7815  modom  8712  dffin7-2  9814  algcvgblem  15917  divgcdodd  16050  chrelat2i  30146  disjex  30348  disjexc  30349  meran1  33786  meran3  33788  bj-dfbi5  33934  bj-andnotim  33949  itg2addnclem2  35021  dvasin  35053  impor  35431  biimpor  35434  hlrelat2  36611  ifpim1  40033  ifpim2  40036  ifpidg  40055  ifpim23g  40059  ifpim123g  40064  ifpimimb  40068  ifpororb  40069  sqrtcvallem1  40187  hbimpgVD  41470  stoweidlem14  42522  fvmptrabdm  43715  alimp-surprise  45162  eximp-surprise  45166
  Copyright terms: Public domain W3C validator