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

Theorem orbi1i 520
Description: Inference adding a right disjunct to both sides of a logical equivalence. (Contributed by NM, 3-Jan-1993.)
Hypothesis
Ref Expression
orbi2i.1  |-  ( ph  <->  ps )
Assertion
Ref Expression
orbi1i  |-  ( (
ph  \/  ch )  <->  ( ps  \/  ch )
)

Proof of Theorem orbi1i
StepHypRef Expression
1 orcom 387 . 2  |-  ( (
ph  \/  ch )  <->  ( ch  \/  ph )
)
2 orbi2i.1 . . 3  |-  ( ph  <->  ps )
32orbi2i 519 . 2  |-  ( ( ch  \/  ph )  <->  ( ch  \/  ps )
)
4 orcom 387 . 2  |-  ( ( ch  \/  ps )  <->  ( ps  \/  ch )
)
51, 3, 43bitri 271 1  |-  ( (
ph  \/  ch )  <->  ( ps  \/  ch )
)
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184    \/ wo 368
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 370
This theorem is referenced by:  orbi12i  521  orordi  530  jaoi2OLD  962  3anor  984  3or6  1305  cadan  1438  19.45  1914  unass  3654  tz7.48lem  7096  dffin7-2  8767  zorng  8873  entri2  8922  grothprim  9201  leloe  9660  arch  10781  elznn0nn  10867  xrleloe  11339  opsrtoslem1  17912  fctop2  19265  alexsubALTlem3  20277  colinearalg  23882  cusgrasizeindslem2  24136  disjnf  27092  ballotlemfc0  28057  ballotlemfcc  28058  ordcmp  29475  ovoliunnfl  29620  biimpor  30071  tsim1  30128  tsbi4  30134  expdioph  30558  ldepspr  32022  sbc3or  32256  en3lpVD  32600  bj-dfif5ALT  33105  bj-nfn  33182  leatb  33964
  Copyright terms: Public domain W3C validator