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

Theorem orbi1i 914
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 913 . 2 ((𝜒𝜑) ↔ (𝜒𝜓))
4 orcom 870 . 2 ((𝜒𝜓) ↔ (𝜓𝜒))
51, 3, 43bitri 300 1 ((𝜑𝜒) ↔ (𝜓𝜒))
Colors of variables: wff setvar class
Syntax hints:  wb 209  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 210  df-or 848
This theorem is referenced by:  orbi12i  915  orordi  929  3ianor  1109  3or6  1449  norasslem1  1536  norass  1539  cadan  1616  19.45v  2002  19.45  2237  unass  4089  tz7.48lem  8186  dffin7-2  10025  zorng  10131  entri2  10185  grothprim  10461  leloe  10932  arch  12100  elznn0nn  12203  xrleloe  12747  swrdnnn0nd  14234  ressval3d  16811  opsrtoslem1  21025  fctop2  21915  alexsubALTlem3  22959  colinearalg  27014  numclwwlk3lem2  28480  disjnf  30641  ballotlemfc0  32184  ballotlemfcc  32185  satfvsucsuc  33053  satfbrsuc  33054  fmlasuc  33074  otthne  33411  noextenddif  33621  sleloe  33707  ordcmp  34386  wl-df2-3mintru2  35406  poimirlem21  35548  ovoliunnfl  35569  biimpor  35992  tsim1  36038  leatb  37056  metakunt1  39863  expdioph  40563  ifpim123g  40807  ifpimimb  40811  ifpororb  40812  rp-fakeinunass  40822  andi3or  41324  uneqsn  41325  sbc3or  41840  en3lpVD  42153  el1fzopredsuc  44505  iccpartgt  44567  fmtno4prmfac  44712  ldepspr  45502
  Copyright terms: Public domain W3C validator