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

Theorem orbi1d 739
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 738 . 2 (𝜑 → ((𝜃𝜓) ↔ (𝜃𝜒)))
3 orcom 401 . 2 ((𝜓𝜃) ↔ (𝜃𝜓))
4 orcom 401 . 2 ((𝜒𝜃) ↔ (𝜃𝜒))
52, 3, 43bitr4g 303 1 (𝜑 → ((𝜓𝜃) ↔ (𝜒𝜃)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wo 382
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 197  df-or 384
This theorem is referenced by:  orbi1  742  orbi12d  746  eueq2  3413  uneq1  3793  r19.45zv  4101  rexprg  4267  rextpg  4269  swopolem  5073  ordsseleq  5790  ordtri3  5797  infltoreq  8449  cantnflem1  8624  axgroth2  9685  axgroth3  9691  lelttric  10182  ltxr  11987  xmulneg1  12137  fzpr  12434  elfzp12  12457  caubnd  14142  lcmval  15352  lcmass  15374  isprm6  15473  vdwlem10  15741  irredmul  18755  domneq0  19345  opsrval  19522  znfld  19957  logreclem  24545  perfectlem2  25000  legov3  25538  lnhl  25555  colperpex  25670  lmif  25722  islmib  25724  friendshipgt3  27385  h1datom  28569  xrlelttric  29645  tlt3  29793  esumpcvgval  30268  sibfof  30530  segcon2  32337  poimirlem25  33564  cnambfre  33588  pridl  33966  ismaxidl  33969  ispridlc  33999  pridlc  34000  dmnnzd  34004  4atlem3a  35201  pmapjoin  35456  lcfl3  37100  lcfl4N  37101  sbc3orgOLD  39059  fourierdlem80  40721  el1fzopredsuc  41660  perfectALTVlem2  41956  nnsum3primesle9  42007  lindslinindsimp2  42577
  Copyright terms: Public domain W3C validator