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

Theorem orbi1i 520
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 387 . 2  |-  ( (
ph  \/  ch )  <->  ( ch  \/  ph )
)
2 orbi2i.1 . . 3  |-  ( ph  <->  ps )
32orbi2i 519 . 2  |-  ( ( ch  \/  ph )  <->  ( ch  \/  ps )
)
4 orcom 387 . 2  |-  ( ( ch  \/  ps )  <->  ( ps  \/  ch )
)
51, 3, 43bitri 271 1  |-  ( (
ph  \/  ch )  <->  ( ps  \/  ch )
)
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184    \/ wo 368
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 185  df-or 370
This theorem is referenced by:  orbi12i  521  orordi  530  3anor  990  3or6  1311  cadan  1447  19.45  1956  unass  3646  tz7.48lem  7108  dffin7-2  8781  zorng  8887  entri2  8936  grothprim  9215  leloe  9674  arch  10799  elznn0nn  10885  xrleloe  11360  opsrtoslem1  18126  fctop2  19483  alexsubALTlem3  20526  colinearalg  24189  cusgrasizeindslem2  24450  disjnf  27409  ballotlemfc0  28408  ballotlemfcc  28409  ordcmp  29887  ovoliunnfl  30031  biimpor  30456  tsim1  30512  expdioph  30940  ressval3d  32393  ldepspr  32809  sbc3or  33035  en3lpVD  33378  bj-dfif5ALT  33897  bj-nfn  33967  leatb  34757  rp-fakeinunass  37443
  Copyright terms: Public domain W3C validator