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 867 . 2 ((𝜑𝜒) ↔ (𝜒𝜑))
2 orbi2i.1 . . 3 (𝜑𝜓)
32orbi2i 910 . 2 ((𝜒𝜑) ↔ (𝜒𝜓))
4 orcom 867 . 2 ((𝜒𝜓) ↔ (𝜓𝜒))
51, 3, 43bitri 300 1 ((𝜑𝜒) ↔ (𝜓𝜒))
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 209   ∨ wo 844 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 845 This theorem is referenced by:  orbi12i  912  orordi  926  3ianor  1104  3or6  1444  norasslem1  1531  norass  1534  cadan  1611  19.45v  2001  19.45  2242  unass  4126  tz7.48lem  8060  dffin7-2  9805  zorng  9911  entri2  9965  grothprim  10241  leloe  10712  arch  11880  elznn0nn  11981  xrleloe  12523  swrdnnn0nd  14007  ressval3d  16550  opsrtoslem1  20250  fctop2  21599  alexsubALTlem3  22643  colinearalg  26693  numclwwlk3lem2  28158  disjnf  30317  ballotlemfc0  31768  ballotlemfcc  31769  satfvsucsuc  32630  satfbrsuc  32631  fmlasuc  32651  noextenddif  33193  sleloe  33251  ordcmp  33813  poimirlem21  34978  ovoliunnfl  34999  biimpor  35422  tsim1  35468  leatb  36488  metakunt1  39240  expdioph  39796  ifpim123g  40040  ifpimimb  40044  ifpororb  40045  rp-fakeinunass  40055  andi3or  40560  uneqsn  40561  sbc3or  41074  en3lpVD  41387  el1fzopredsuc  43724  iccpartgt  43786  fmtno4prmfac  43931  ldepspr  44723
 Copyright terms: Public domain W3C validator