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

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

Proof of Theorem orbi1i
StepHypRef Expression
1 orcom 377 . 2  |-  ( (
ph  \/  ch )  <->  ( ch  \/  ph )
)
2 orbi2i.1 . . 3  |-  ( ph  <->  ps )
32orbi2i 506 . 2  |-  ( ( ch  \/  ph )  <->  ( ch  \/  ps )
)
4 orcom 377 . 2  |-  ( ( ch  \/  ps )  <->  ( ps  \/  ch )
)
51, 3, 43bitri 263 1  |-  ( (
ph  \/  ch )  <->  ( ps  \/  ch )
)
Colors of variables: wff set class
Syntax hints:    <-> wb 177    \/ wo 358
This theorem is referenced by:  orbi12i  508  orordi  517  jaoi2  934  3anor  950  3or6  1265  19.45  1895  unass  3464  tz7.48lem  6657  dffin7-2  8234  zorng  8340  entri2  8389  grothprim  8665  leloe  9117  arch  10174  elznn0nn  10251  xrleloe  10693  opsrtoslem1  16499  fctop2  17024  alexsubALTlem3  18033  cusgrasizeindslem2  21436  ballotlemfc0  24703  ballotlemfcc  24704  colinearalg  25753  ordcmp  26101  ovoliunnfl  26147  expdioph  26984  en3lpVD  28666  leatb  29775
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