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

Theorem orbi1i 506
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 376 . 2  |-  ( (
ph  \/  ch )  <->  ( ch  \/  ph )
)
2 orbi2i.1 . . 3  |-  ( ph  <->  ps )
32orbi2i 505 . 2  |-  ( ( ch  \/  ph )  <->  ( ch  \/  ps )
)
4 orcom 376 . 2  |-  ( ( ch  \/  ps )  <->  ( ps  \/  ch )
)
51, 3, 43bitri 262 1  |-  ( (
ph  \/  ch )  <->  ( ps  \/  ch )
)
Colors of variables: wff set class
Syntax hints:    <-> wb 176    \/ wo 357
This theorem is referenced by:  orbi12i  507  orordi  516  3anor  948  3or6  1263  19.45  1814  unass  3332  tz7.48lem  6453  dffin7-2  8024  zorng  8131  entri2  8180  grothprim  8456  leloe  8908  arch  9962  elznn0nn  10037  xrleloe  10478  opsrtoslem1  16225  fctop2  16742  alexsubALTlem3  17743  ballotlemfc0  23051  ballotlemfcc  23052  colinearalg  24538  ordcmp  24886  anddi2  24941  expdioph  27116  en3lpVD  28621  leatb  29482
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 177  df-or 359
  Copyright terms: Public domain W3C validator