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

Theorem orbi1d 916
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 915 . 2 (𝜑 → ((𝜃𝜓) ↔ (𝜃𝜒)))
3 orcom 869 . 2 ((𝜓𝜃) ↔ (𝜃𝜓))
4 orcom 869 . 2 ((𝜒𝜃) ↔ (𝜃𝜒))
52, 3, 43bitr4g 314 1 (𝜑 → ((𝜓𝜃) ↔ (𝜒𝜃)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wo 846
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 847
This theorem is referenced by:  orbi1  917  orbi12d  918  eueq2  3667  uneq1  4115  r19.45zv  4459  rexprgf  4653  rextpg  4659  swopolem  5553  ordsseleq  6343  ordtri3  6350  infltoreq  9372  cantnflem1  9559  axgroth2  10695  axgroth3  10701  lelttric  11196  ltxr  12965  xmulneg1  13117  fzpr  13425  elfzp12  13449  caubnd  15178  lcmval  16403  lcmass  16425  isprm6  16525  vdwlem10  16797  irredmul  20062  domneq0  20691  znfld  20891  opsrval  21370  logreclem  26035  perfectlem2  26501  legov3  27339  lnhl  27356  colperpex  27474  lmif  27526  islmib  27528  friendshipgt3  29141  h1datom  30323  xrlelttric  31452  tlt3  31625  prmidl  32002  ismxidl  32021  esumpcvgval  32451  sibfof  32714  satfvsuc  33729  satfv1  33731  satfvsucsuc  33733  satf0suc  33744  sat1el2xp  33747  fmlasuc0  33752  fmlafvel  33753  satfv1fvfmla1  33791  frxp2  34180  xpord2pred  34181  xpord2ind  34183  frxp3  34186  xpord3pred  34187  segcon2  34586  wl-ifpimpr  35833  poimirlem25  35999  cnambfre  36022  pridl  36392  ismaxidl  36395  ispridlc  36425  pridlc  36426  dmnnzd  36430  disjecxrncnvep  36748  4atlem3a  37956  pmapjoin  38211  lcfl3  39853  lcfl4N  39854  sticksstones22  40472  sbcoreleleqVD  42906  fourierdlem80  44182  euoreqb  45096  el1fzopredsuc  45312  perfectALTVlem2  45669  nnsum3primesle9  45741  lindslinindsimp2  46299
  Copyright terms: Public domain W3C validator