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  1888  unass  3440  tz7.48lem  6627  dffin7-2  8204  zorng  8310  entri2  8359  grothprim  8635  leloe  9087  arch  10143  elznn0nn  10220  xrleloe  10662  opsrtoslem1  16464  fctop2  16985  alexsubALTlem3  17994  cusgrasizeindslem2  21342  ballotlemfc0  24522  ballotlemfcc  24523  colinearalg  25556  ordcmp  25904  ovoliunnfl  25946  expdioph  26778  en3lpVD  28291  leatb  29458
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