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

Theorem orbi1i 911
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 868 . 2 ((𝜑𝜒) ↔ (𝜒𝜑))
2 orbi2i.1 . . 3 (𝜑𝜓)
32orbi2i 910 . 2 ((𝜒𝜑) ↔ (𝜒𝜓))
4 orcom 868 . 2 ((𝜒𝜓) ↔ (𝜓𝜒))
51, 3, 43bitri 296 1 ((𝜑𝜒) ↔ (𝜓𝜒))
Colors of variables: wff setvar class
Syntax hints:  wb 205  wo 845
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 206  df-or 846
This theorem is referenced by:  orbi12i  912  orordi  926  3ianor  1104  3or6  1443  norasslem1  1527  norass  1530  cadan  1602  19.45v  1989  19.45  2226  unass  4164  tz7.48lem  8462  dffin7-2  10423  zorng  10529  entri2  10583  grothprim  10859  leloe  11332  arch  12502  elznn0nn  12605  xrleloe  13158  swrdnnn0nd  14642  ressval3d  17230  ressval3dOLD  17231  opsrtoslem1  22021  fctop2  22952  alexsubALTlem3  23997  noextenddif  27647  sleloe  27733  precsexlem11  28165  eln0s  28273  colinearalg  28793  numclwwlk3lem2  30266  disjnf  32439  ballotlemfc0  34243  ballotlemfcc  34244  satfvsucsuc  35106  satfbrsuc  35107  fmlasuc  35127  ordcmp  36062  wl-df2-3mintru2  37095  poimirlem21  37245  ovoliunnfl  37266  biimpor  37688  tsim1  37734  leatb  38894  metakunt1  41791  expdioph  42586  dflim5  42900  ifpim123g  43072  ifpimimb  43076  ifpororb  43077  rp-fakeinunass  43087  andi3or  43596  uneqsn  43597  sbc3or  44113  en3lpVD  44426  el1fzopredsuc  46843  iccpartgt  46904  fmtno4prmfac  47049  dfvopnbgr2  47325  ldepspr  47727
  Copyright terms: Public domain W3C validator