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 303 . . 3 (𝜑 ↔ ¬ ¬ 𝜑)
21imbi1i 338 . 2 ((𝜑𝜓) ↔ (¬ ¬ 𝜑𝜓))
3 df-or 384 . 2 ((¬ 𝜑𝜓) ↔ (¬ ¬ 𝜑𝜓))
42, 3bitr4i 266 1 ((𝜑𝜓) ↔ (¬ 𝜑𝜓))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 195   ∨ 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 196  df-or 384 This theorem is referenced by:  imori  428  imorri  429  pm4.62  434  pm4.52  511  pm4.78  604  dfifp4  1010  dfifp5  1011  dfifp7  1013  rb-bijust  1665  rb-imdf  1666  rb-ax1  1668  nf2  1702  r19.30  3063  soxp  7177  modom  8046  dffin7-2  9103  algcvgblem  15128  divgcdodd  15260  chrelat2i  28608  disjex  28787  disjexc  28788  meran1  31580  meran3  31582  bj-dfbi5  31729  bj-andnotim  31746  bj-nf2  31766  itg2addnclem2  32632  dvasin  32666  impor  33050  biimpor  33053  hlrelat2  33707  ifpim1  36832  ifpim2  36835  ifpidg  36855  ifpim23g  36859  ifpim123g  36864  ifpimimb  36868  ifpororb  36869  hbimpgVD  38162  stoweidlem14  38907  alimp-surprise  42335  eximp-surprise  42339
 Copyright terms: Public domain W3C validator