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

Theorem orbi1i 907
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 864 . 2 ((𝜑𝜒) ↔ (𝜒𝜑))
2 orbi2i.1 . . 3 (𝜑𝜓)
32orbi2i 906 . 2 ((𝜒𝜑) ↔ (𝜒𝜓))
4 orcom 864 . 2 ((𝜒𝜓) ↔ (𝜓𝜒))
51, 3, 43bitri 298 1 ((𝜑𝜒) ↔ (𝜓𝜒))
Colors of variables: wff setvar class
Syntax hints:  wb 207  wo 841
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 208  df-or 842
This theorem is referenced by:  orbi12i  908  orordi  922  3ianor  1099  3or6  1438  norasslem1  1521  norass  1524  cadan  1601  19.45v  1991  19.45  2230  unass  4139  tz7.48lem  8066  dffin7-2  9808  zorng  9914  entri2  9968  grothprim  10244  leloe  10715  arch  11882  elznn0nn  11983  xrleloe  12525  swrdnnn0nd  14006  ressval3d  16549  opsrtoslem1  20192  fctop2  21541  alexsubALTlem3  22585  colinearalg  26623  numclwwlk3lem2  28090  disjnf  30248  ballotlemfc0  31649  ballotlemfcc  31650  satfvsucsuc  32509  satfbrsuc  32510  fmlasuc  32530  noextenddif  33072  sleloe  33130  ordcmp  33692  poimirlem21  34794  ovoliunnfl  34815  biimpor  35243  tsim1  35289  leatb  36308  expdioph  39498  ifpim123g  39744  ifpimimb  39748  ifpororb  39749  rp-fakeinunass  39759  andi3or  40250  uneqsn  40251  sbc3or  40743  en3lpVD  41056  el1fzopredsuc  43402  iccpartgt  43464  fmtno4prmfac  43611  ldepspr  44456
  Copyright terms: Public domain W3C validator