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

Theorem orbi1i 913
Description: Inference adding a right disjunct to both sides of a logical equivalence. (Contributed by NM, 3-Jan-1993.)
Hypothesis
Ref Expression
orbi2i.1 (𝜑𝜓)
Assertion
Ref Expression
orbi1i ((𝜑𝜒) ↔ (𝜓𝜒))

Proof of Theorem orbi1i
StepHypRef Expression
1 orcom 870 . 2 ((𝜑𝜒) ↔ (𝜒𝜑))
2 orbi2i.1 . . 3 (𝜑𝜓)
32orbi2i 912 . 2 ((𝜒𝜑) ↔ (𝜒𝜓))
4 orcom 870 . 2 ((𝜒𝜓) ↔ (𝜓𝜒))
51, 3, 43bitri 297 1 ((𝜑𝜒) ↔ (𝜓𝜒))
Colors of variables: wff setvar class
Syntax hints:  wb 206  wo 847
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 207  df-or 848
This theorem is referenced by:  orbi12i  914  orordi  928  3ianor  1106  3or6  1448  norasslem1  1533  norass  1536  cadan  1608  19.45v  1992  19.45  2237  unass  4171  tz7.48lem  8482  dffin7-2  10439  zorng  10545  entri2  10599  grothprim  10875  leloe  11348  arch  12525  elznn0nn  12629  xrleloe  13187  swrdnnn0nd  14695  ressval3d  17293  opsrtoslem1  22080  fctop2  23013  alexsubALTlem3  24058  noextenddif  27714  sleloe  27800  precsexlem11  28242  eln0s  28359  colinearalg  28926  numclwwlk3lem2  30404  disjnf  32584  ballotlemfc0  34496  ballotlemfcc  34497  satfvsucsuc  35371  satfbrsuc  35372  fmlasuc  35392  ordcmp  36449  wl-df2-3mintru2  37487  poimirlem21  37649  ovoliunnfl  37670  biimpor  38092  tsim1  38138  leatb  39294  metakunt1  42207  expdioph  43040  dflim5  43347  ifpim123g  43518  ifpimimb  43522  ifpororb  43523  rp-fakeinunass  43533  andi3or  44042  uneqsn  44043  sbc3or  44557  en3lpVD  44870  el1fzopredsuc  47342  iccpartgt  47419  fmtno4prmfac  47564  dfvopnbgr2  47844  isubgr3stgrlem4  47941  ldepspr  48395
  Copyright terms: Public domain W3C validator