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

Theorem orbi1d 910
Description: Deduction adding a right disjunct to both sides of a logical equivalence. (Contributed by NM, 21-Jun-1993.)
Hypothesis
Ref Expression
bid.1 (𝜑 → (𝜓𝜒))
Assertion
Ref Expression
orbi1d (𝜑 → ((𝜓𝜃) ↔ (𝜒𝜃)))

Proof of Theorem orbi1d
StepHypRef Expression
1 bid.1 . . 3 (𝜑 → (𝜓𝜒))
21orbi2d 909 . 2 (𝜑 → ((𝜃𝜓) ↔ (𝜃𝜒)))
3 orcom 864 . 2 ((𝜓𝜃) ↔ (𝜃𝜓))
4 orcom 864 . 2 ((𝜒𝜃) ↔ (𝜃𝜒))
52, 3, 43bitr4g 315 1 (𝜑 → ((𝜓𝜃) ↔ (𝜒𝜃)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  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:  orbi1  911  orbi12d  912  eueq2  3698  uneq1  4129  r19.45zv  4444  rexprgf  4623  rextpg  4627  swopolem  5476  ordsseleq  6213  ordtri3  6220  infltoreq  8954  cantnflem1  9140  axgroth2  10235  axgroth3  10241  lelttric  10735  ltxr  12498  xmulneg1  12650  fzpr  12950  elfzp12  12974  caubnd  14706  lcmval  15924  lcmass  15946  isprm6  16046  vdwlem10  16314  irredmul  19388  domneq0  19998  opsrval  20183  znfld  20635  logreclem  25267  perfectlem2  25733  legov3  26311  lnhl  26328  colperpex  26446  lmif  26498  islmib  26500  friendshipgt3  28104  h1datom  29286  xrlelttric  30402  tlt3  30579  prmidl  30876  esumpcvgval  31236  sibfof  31497  satfvsuc  32505  satfv1  32507  satfvsucsuc  32509  satf0suc  32520  sat1el2xp  32523  fmlasuc0  32528  fmlafvel  32529  satfv1fvfmla1  32567  segcon2  33463  poimirlem25  34798  cnambfre  34821  pridl  35196  ismaxidl  35199  ispridlc  35229  pridlc  35230  dmnnzd  35234  4atlem3a  36613  pmapjoin  36868  lcfl3  38510  lcfl4N  38511  sbcoreleleqVD  41070  fourierdlem80  42348  euoreqb  43185  el1fzopredsuc  43402  perfectALTVlem2  43764  nnsum3primesle9  43836  lindslinindsimp2  44446
  Copyright terms: Public domain W3C validator