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

Theorem orbi1d 734
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 733 . 2 (𝜑 → ((𝜃𝜓) ↔ (𝜃𝜒)))
3 orcom 400 . 2 ((𝜓𝜃) ↔ (𝜃𝜓))
4 orcom 400 . 2 ((𝜒𝜃) ↔ (𝜃𝜒))
52, 3, 43bitr4g 301 1 (𝜑 → ((𝜓𝜃) ↔ (𝜒𝜃)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194  wo 381
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 195  df-or 383
This theorem is referenced by:  orbi1  737  orbi12d  741  eueq2  3346  uneq1  3721  r19.45zv  4019  rexprg  4181  rextpg  4183  swopolem  4958  ordsseleq  5655  ordtri3  5662  infltoreq  8268  cantnflem1  8446  axgroth2  9503  axgroth3  9509  lelttric  9995  ltxr  11784  xmulneg1  11928  fzpr  12221  elfzp12  12243  caubnd  13892  lcmval  15089  lcmass  15111  isprm6  15210  vdwlem10  15478  irredmul  18478  domneq0  19064  opsrval  19241  znfld  19673  logreclem  24217  perfectlem2  24672  legov3  25211  lnhl  25228  colperpex  25343  lmif  25395  islmib  25397  friendshipgt3  26414  h1datom  27631  xrlelttric  28712  tlt3  28802  esumpcvgval  29273  sibfof  29535  nofulllem5  30911  segcon2  31188  poimirlem25  32400  cnambfre  32424  pridl  32802  ismaxidl  32805  ispridlc  32835  pridlc  32836  dmnnzd  32840  4atlem3a  33697  pmapjoin  33952  lcfl3  35597  lcfl4N  35598  sbc3orgOLD  37559  fourierdlem80  38876  el1fzopredsuc  39746  perfectALTVlem2  39963  nnsum3primesle9  40008  av-friendshipgt3  41547  lindslinindsimp2  42041
  Copyright terms: Public domain W3C validator