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

Theorem orbi2d 911
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 342 . 2 (𝜑 → ((¬ 𝜃𝜓) ↔ (¬ 𝜃𝜒)))
3 df-or 844 . 2 ((𝜃𝜓) ↔ (¬ 𝜃𝜓))
4 df-or 844 . 2 ((𝜃𝜒) ↔ (¬ 𝜃𝜒))
52, 3, 43bitr4g 315 1 (𝜑 → ((𝜃𝜓) ↔ (𝜃𝜒)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 207  wo 843
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 208  df-or 844
This theorem is referenced by:  orbi1d  912  orbi12d  914  eueq2  3704  sbc2or  3784  r19.44zv  4451  rexprgf  4629  rextpg  4633  swopolem  5481  poleloe  5988  elsucg  6255  elsuc2g  6256  brdifun  8311  brwdom  9023  isfin1a  9706  elgch  10036  suplem2pr  10467  axlttri  10704  mulcan1g  11285  elznn0  11988  elznn  11989  zindd  12075  rpneg  12414  dfle2  12533  fzm1  12980  fzosplitsni  13141  hashv01gt1  13698  zeo5  15697  bitsf1  15787  lcmval  15928  lcmneg  15939  lcmass  15950  isprm6  16050  infpn2  16241  irredmul  19381  domneq0  19991  znfld  20623  quotval  24796  plydivlem4  24800  plydivex  24801  aalioulem2  24837  aalioulem5  24840  aalioulem6  24841  aaliou  24842  aaliou2  24844  aaliou2b  24845  isinag  26539  axcontlem7  26671  hashecclwwlkn1  27771  elunsn  30188  eliccioo  30522  tlt2  30566  prmidl  30864  sibfof  31485  ballotlemfc0  31637  ballotlemfcc  31638  satfvsucsuc  32497  satf0op  32509  fmlafvel  32517  isfmlasuc  32520  satfv1fvfmla1  32555  seglelin  33462  lineunray  33493  topdifinfeq  34501  mblfinlem2  34798  pridl  35184  maxidlval  35186  ispridlc  35217  pridlc  35218  dmnnzd  35222  lcfl7N  38505  aomclem8  39523  orbi1r  40706  iccpartgtl  43415  iccpartleu  43417  lindslinindsimp2lem5  44346  lindslinindsimp2  44347  rrx2pnedifcoorneorr  44533
  Copyright terms: Public domain W3C validator