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  jaoi2OLD  960  3anor  981  3or6  1301  cadan  1434  19.45  1910  unass  3622  tz7.48lem  7007  dffin7-2  8679  zorng  8785  entri2  8834  grothprim  9113  leloe  9573  arch  10688  elznn0nn  10772  xrleloe  11233  opsrtoslem1  17690  fctop2  18742  alexsubALTlem3  19754  colinearalg  23309  cusgrasizeindslem2  23535  disjnf  26068  ballotlemfc0  27020  ballotlemfcc  27021  ordcmp  28438  ovoliunnfl  28582  biimpor  29033  tsim1  29090  tsbi4  29096  expdioph  29521  ldepspr  31140  sbc3or  31570  en3lpVD  31914  bj-dfif5ALT  32419  bj-nfn  32494  leatb  33276
  Copyright terms: Public domain W3C validator