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  1800  r19.30  2685  soxp  6228  modom  7063  dffin7-2  8024  algcvgblem  12747  divgcdodd  12798  chrelat2i  22945  disjex  23176  disjexc  23177  meran1  24850  meran3  24852  dvreasin  24923  clsbldimp  25088  stoweidlem14  27763  hbimpgVD  28680  hlrelat2  29592
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