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  3441  tz7.48lem  6628  dffin7-2  8205  zorng  8311  entri2  8360  grothprim  8636  leloe  9088  arch  10144  elznn0nn  10221  xrleloe  10663  opsrtoslem1  16465  fctop2  16986  alexsubALTlem3  17995  cusgrasizeindslem2  21343  ballotlemfc0  24523  ballotlemfcc  24524  colinearalg  25557  ordcmp  25905  ovoliunnfl  25947  expdioph  26779  en3lpVD  28292  leatb  29459
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