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

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

Proof of Theorem imor
StepHypRef Expression
1 notnot 282 . . 3  |-  ( ph  <->  -. 
-.  ph )
21imbi1i 315 . 2  |-  ( (
ph  ->  ps )  <->  ( -.  -.  ph  ->  ps )
)
3 df-or 359 . 2  |-  ( ( -.  ph  \/  ps ) 
<->  ( -.  -.  ph  ->  ps ) )
42, 3bitr4i 243 1  |-  ( (
ph  ->  ps )  <->  ( -.  ph  \/  ps ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 176    \/ wo 357
This theorem is referenced by:  imori  402  imorri  403  pm4.62  408  pm4.52  477  pm4.78  565  rb-bijust  1504  rb-imdf  1505  rb-ax1  1507  nf4  1812  r19.30  2698  soxp  6244  modom  7079  dffin7-2  8040  algcvgblem  12763  divgcdodd  12814  chrelat2i  22961  disjex  23192  disjexc  23193  meran1  24922  meran3  24924  itg2addnclem2  25004  dvreasin  25026  clsbldimp  25191  stoweidlem14  27866  hbimpgVD  28996  hlrelat2  30214
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-or 359
  Copyright terms: Public domain W3C validator