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  1826  unass  3345  tz7.48lem  6469  dffin7-2  8040  zorng  8147  entri2  8196  grothprim  8472  leloe  8924  arch  9978  elznn0nn  10053  xrleloe  10494  opsrtoslem1  16241  fctop2  16758  alexsubALTlem3  17759  ballotlemfc0  23067  ballotlemfcc  23068  colinearalg  24609  ordcmp  24957  ovoliunnfl  25000  anddi2  25043  expdioph  27218  jaoi2  28175  en3lpVD  28936  leatb  30104
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