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

Theorem imor 402
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 283 . . 3  |-  ( ph  <->  -. 
-.  ph )
21imbi1i 316 . 2  |-  ( (
ph  ->  ps )  <->  ( -.  -.  ph  ->  ps )
)
3 df-or 360 . 2  |-  ( ( -.  ph  \/  ps ) 
<->  ( -.  -.  ph  ->  ps ) )
42, 3bitr4i 244 1  |-  ( (
ph  ->  ps )  <->  ( -.  ph  \/  ps ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 177    \/ wo 358
This theorem is referenced by:  imori  403  imorri  404  pm4.62  409  pm4.52  478  pm4.78  566  rb-bijust  1523  rb-imdf  1524  rb-ax1  1526  nf4  1891  r19.30  2845  soxp  6450  modom  7300  dffin7-2  8267  algcvgblem  13056  divgcdodd  13107  chrelat2i  23856  disjex  24020  disjexc  24021  meran1  26109  meran3  26111  itg2addnclem2  26203  dvreasin  26226  stoweidlem14  27677  hbimpgVD  28870  hlrelat2  30039
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 178  df-or 360
  Copyright terms: Public domain W3C validator