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  1626  rb-imdf  1627  rb-ax1  1629  nf4  2020  r19.30  2912  soxp  6864  modom  7726  dffin7-2  8779  algcvgblem  14479  divgcdodd  14596  chrelat2i  27960  disjex  28148  disjexc  28149  meran1  31020  meran3  31022  bj-dfbi5  31099  bj-andnotim  31120  bj-nf2  31140  itg2addnclem2  31901  dvasin  31935  impor  32221  biimpor  32224  hlrelat2  32880  ifpim1  36025  ifpim2  36028  ifpidg  36048  ifpim23g  36052  ifpim123g  36057  ifpimimb  36061  ifpororb  36062  hbimpgVD  37217  stoweidlem14  37757  alimp-surprise  40122  eximp-surprise  40126
  Copyright terms: Public domain W3C validator