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

Theorem imor 852
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 847 . 2 ((¬ 𝜑𝜓) ↔ (¬ ¬ 𝜑𝜓))
42, 3bitr4i 281 1 ((𝜑𝜓) ↔ (¬ 𝜑𝜓))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 209  wo 846
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 847
This theorem is referenced by:  imori  853  imorri  854  pm4.62  855  pm4.78  934  pm4.52  984  dfifp4  1066  dfifp5  1067  dfifp7  1069  norasslem1  1535  rb-bijust  1756  rb-imdf  1757  rb-ax1  1759  nf2  1792  relsnb  5640  soxp  7842  modom  8791  dffin7-2  9891  algcvgblem  16011  divgcdodd  16144  chrelat2i  30292  disjex  30497  disjexc  30498  noinfprefixmo  33537  meran1  34230  meran3  34232  bj-dfbi5  34382  bj-andnotim  34397  itg2addnclem2  35441  dvasin  35473  impor  35851  biimpor  35854  hlrelat2  37029  sticksstones1  39697  flt4lem7  40052  nna4b4nsq  40053  ifpim1  40614  ifpim2  40617  ifpidg  40636  ifpim23g  40640  ifpim123g  40645  ifpimimb  40649  ifpororb  40650  sqrtcvallem1  40768  hbimpgVD  42046  stoweidlem14  43081  fvmptrabdm  44302  alimp-surprise  45921  eximp-surprise  45925
  Copyright terms: Public domain W3C validator