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

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

Proof of Theorem orbi2d
StepHypRef Expression
1 bid.1 . . 3 (𝜑 → (𝜓𝜒))
21imbi2d 332 . 2 (𝜑 → ((¬ 𝜃𝜓) ↔ (¬ 𝜃𝜒)))
3 df-or 875 . 2 ((𝜃𝜓) ↔ (¬ 𝜃𝜓))
4 df-or 875 . 2 ((𝜃𝜒) ↔ (¬ 𝜃𝜒))
52, 3, 43bitr4g 306 1 (𝜑 → ((𝜃𝜓) ↔ (𝜃𝜒)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 198  wo 874
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 199  df-or 875
This theorem is referenced by:  orbi1d  941  orbi12d  943  eueq2  3576  sbc2or  3642  r19.44zv  4262  rexprg  4425  rextpg  4427  swopolem  5242  poleloe  5745  elsucg  6008  elsuc2g  6009  brdifun  8011  brwdom  8714  isfin1a  9402  elgch  9732  suplem2pr  10163  axlttri  10399  mulcan1g  10972  elznn0  11681  elznn  11682  zindd  11768  rpneg  12108  dfle2  12227  fzm1  12674  fzosplitsni  12834  hashv01gt1  13385  zeo5  15416  bitsf1  15503  lcmval  15640  lcmneg  15651  lcmass  15662  isprm6  15759  infpn2  15950  irredmul  19025  domneq0  19620  znfld  20230  quotval  24388  plydivlem4  24392  plydivex  24393  aalioulem2  24429  aalioulem5  24432  aalioulem6  24433  aaliou  24434  aaliou2  24436  aaliou2b  24437  isinag  26085  axcontlem7  26207  hashecclwwlkn1  27395  eliccioo  30155  tlt2  30180  sibfof  30918  ballotlemfc0  31071  ballotlemfcc  31072  seglelin  32736  lineunray  32767  topdifinfeq  33696  mblfinlem2  33936  pridl  34323  maxidlval  34325  ispridlc  34356  pridlc  34357  dmnnzd  34361  lcfl7N  37522  aomclem8  38416  orbi1r  39496  iccpartgtl  42202  iccpartleu  42204  lindslinindsimp2lem5  43050  lindslinindsimp2  43051
  Copyright terms: Public domain W3C validator