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  12966  xmulneg1  13118  fzpr  13426  elfzp12  13450  caubnd  15179  lcmval  16404  lcmass  16426  isprm6  16526  vdwlem10  16798  irredmul  20067  domneq0  20696  znfld  20896  opsrval  21375  logreclem  26040  perfectlem2  26506  legov3  27345  lnhl  27362  colperpex  27480  lmif  27532  islmib  27534  friendshipgt3  29147  h1datom  30329  xrlelttric  31458  tlt3  31631  prmidl  32008  ismxidl  32027  esumpcvgval  32457  sibfof  32720  satfvsuc  33735  satfv1  33737  satfvsucsuc  33739  satf0suc  33750  sat1el2xp  33753  fmlasuc0  33758  fmlafvel  33759  satfv1fvfmla1  33797  frxp2  34183  xpord2pred  34184  xpord2ind  34186  frxp3  34189  xpord3pred  34190  segcon2  34621  wl-ifpimpr  35868  poimirlem25  36034  cnambfre  36057  pridl  36427  ismaxidl  36430  ispridlc  36460  pridlc  36461  dmnnzd  36465  disjecxrncnvep  36783  4atlem3a  37991  pmapjoin  38246  lcfl3  39888  lcfl4N  39889  sticksstones22  40507  sbcoreleleqVD  42942  fourierdlem80  44218  euoreqb  45132  el1fzopredsuc  45348  perfectALTVlem2  45705  nnsum3primesle9  45777  lindslinindsimp2  46335
  Copyright terms: Public domain W3C validator