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

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

Proof of Theorem orbi1i
StepHypRef Expression
1 orcom 388 . 2  |-  ( (
ph  \/  ch )  <->  ( ch  \/  ph )
)
2 orbi2i.1 . . 3  |-  ( ph  <->  ps )
32orbi2i 521 . 2  |-  ( ( ch  \/  ph )  <->  ( ch  \/  ps )
)
4 orcom 388 . 2  |-  ( ( ch  \/  ps )  <->  ( ps  \/  ch )
)
51, 3, 43bitri 274 1  |-  ( (
ph  \/  ch )  <->  ( ps  \/  ch )
)
Colors of variables: wff setvar class
Syntax hints:    <-> wb 187    \/ wo 369
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 188  df-or 371
This theorem is referenced by:  orbi12i  523  orordi  532  3anor  998  3or6  1346  cadan  1507  19.45v  1818  19.45  2025  unass  3623  tz7.48lem  7163  dffin7-2  8829  zorng  8935  entri2  8984  grothprim  9260  leloe  9721  arch  10867  elznn0nn  10952  xrleloe  11444  ressval3d  15174  opsrtoslem1  18695  fctop2  20007  alexsubALTlem3  21051  colinearalg  24927  cusgrasizeindslem2  25188  disjnf  28171  ballotlemfc0  29321  ballotlemfcc  29322  ordcmp  31100  bj-nfn  31206  poimirlem21  31875  ovoliunnfl  31896  biimpor  32231  tsim1  32286  leatb  32777  expdioph  35798  ifpim123g  36064  ifpimimb  36068  ifpororb  36069  rp-fakeinunass  36080  sbc3or  36747  en3lpVD  37102  el1fzopredsuc  38434  iccpartgt  38453  ldepspr  39540
  Copyright terms: Public domain W3C validator