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

Theorem imor 427
 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 304 . . 3 (𝜑 ↔ ¬ ¬ 𝜑)
21imbi1i 338 . 2 ((𝜑𝜓) ↔ (¬ ¬ 𝜑𝜓))
3 df-or 384 . 2 ((¬ 𝜑𝜓) ↔ (¬ ¬ 𝜑𝜓))
42, 3bitr4i 267 1 ((𝜑𝜓) ↔ (¬ 𝜑𝜓))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 196   ∨ wo 382 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 197  df-or 384 This theorem is referenced by:  imori  428  imorri  429  pm4.62  434  pm4.52  511  pm4.78  605  dfifp4  1036  dfifp5  1037  dfifp7  1039  rb-bijust  1714  rb-imdf  1715  rb-ax1  1717  nf2  1751  r19.30  3111  soxp  7335  modom  8202  dffin7-2  9258  algcvgblem  15337  divgcdodd  15469  chrelat2i  29352  disjex  29531  disjexc  29532  meran1  32535  meran3  32537  bj-dfbi5  32684  bj-andnotim  32698  itg2addnclem2  33592  dvasin  33626  impor  34010  biimpor  34013  hlrelat2  35007  ifpim1  38130  ifpim2  38133  ifpidg  38153  ifpim23g  38157  ifpim123g  38162  ifpimimb  38166  ifpororb  38167  hbimpgVD  39454  stoweidlem14  40549  fvmptrabdm  41632  alimp-surprise  42854  eximp-surprise  42858
 Copyright terms: Public domain W3C validator