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

Theorem imor 410
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 289 . . 3  |-  ( ph  <->  -. 
-.  ph )
21imbi1i 323 . 2  |-  ( (
ph  ->  ps )  <->  ( -.  -.  ph  ->  ps )
)
3 df-or 368 . 2  |-  ( ( -.  ph  \/  ps ) 
<->  ( -.  -.  ph  ->  ps ) )
42, 3bitr4i 252 1  |-  ( (
ph  ->  ps )  <->  ( -.  ph  \/  ps ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 184    \/ wo 366
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 185  df-or 368
This theorem is referenced by:  imori  411  imorri  412  pm4.62  417  pm4.52  489  pm4.78  580  dfifp4  1386  dfifp5  1387  dfifp7  1389  rb-bijust  1586  rb-imdf  1587  rb-ax1  1589  nf4  1967  r19.30  2999  soxp  6886  modom  7713  dffin7-2  8769  algcvgblem  14290  divgcdodd  14344  chrelat2i  27482  disjex  27662  disjexc  27663  meran1  30104  meran3  30106  itg2addnclem2  30307  dvasin  30343  impor  30718  biimpor  30721  stoweidlem14  32035  alimp-surprise  33583  eximp-surprise  33587  hbimpgVD  34105  bj-dfbi5  34556  bj-andnotim  34578  bj-nf2  34597  hlrelat2  35524  ifpim123g  38103  ifpidg  38105  ifpim1  38110  ifpim2  38111  ifpim23g  38112  ifpimimb  38116  ifpororb  38133
  Copyright terms: Public domain W3C validator