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

Theorem imor 413
Description: Implication in terms of disjunction. Theorem *4.6 of [WhiteheadRussell] p. 120. (Contributed by NM, 3-Jan-1993.)
Assertion
Ref Expression
imor  |-  ( (
ph  ->  ps )  <->  ( -.  ph  \/  ps ) )

Proof of Theorem imor
StepHypRef Expression
1 notnot 292 . . 3  |-  ( ph  <->  -. 
-.  ph )
21imbi1i 326 . 2  |-  ( (
ph  ->  ps )  <->  ( -.  -.  ph  ->  ps )
)
3 df-or 371 . 2  |-  ( ( -.  ph  \/  ps ) 
<->  ( -.  -.  ph  ->  ps ) )
42, 3bitr4i 255 1  |-  ( (
ph  ->  ps )  <->  ( -.  ph  \/  ps ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 187    \/ wo 369
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 188  df-or 371
This theorem is referenced by:  imori  414  imorri  415  pm4.62  420  pm4.52  493  pm4.78  584  dfifp4  1424  dfifp5  1425  dfifp7  1427  rb-bijust  1628  rb-imdf  1629  rb-ax1  1631  nf4  2020  r19.30  2980  soxp  6920  modom  7779  dffin7-2  8826  algcvgblem  14507  divgcdodd  14624  chrelat2i  27853  disjex  28041  disjexc  28042  meran1  30856  meran3  30858  bj-dfbi5  30935  bj-andnotim  30956  bj-nf2  30975  itg2addnclem2  31698  dvasin  31732  impor  32018  biimpor  32021  hlrelat2  32677  ifpim1  35811  ifpim2  35814  ifpidg  35834  ifpim23g  35838  ifpim123g  35843  ifpimimb  35847  ifpororb  35848  hbimpgVD  36941  stoweidlem14  37443  alimp-surprise  39280  eximp-surprise  39284
  Copyright terms: Public domain W3C validator