ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  imbi1d GIF version

Theorem imbi1d 229
Description: Deduction adding a consequent to both sides of a logical equivalence. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 17-Sep-2013.)
Hypothesis
Ref Expression
imbid.1 (𝜑 → (𝜓𝜒))
Assertion
Ref Expression
imbi1d (𝜑 → ((𝜓𝜃) ↔ (𝜒𝜃)))

Proof of Theorem imbi1d
StepHypRef Expression
1 imbid.1 . . . 4 (𝜑 → (𝜓𝜒))
21biimprd 156 . . 3 (𝜑 → (𝜒𝜓))
32imim1d 74 . 2 (𝜑 → ((𝜓𝜃) → (𝜒𝜃)))
41biimpd 142 . . 3 (𝜑 → (𝜓𝜒))
54imim1d 74 . 2 (𝜑 → ((𝜒𝜃) → (𝜓𝜃)))
63, 5impbid 127 1 (𝜑 → ((𝜓𝜃) ↔ (𝜒𝜃)))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 103
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  imbi12d  232  imbi1  234  imim21b  250  pm5.33  574  imordc  832  drsb1  1724  ax11v2  1745  ax11v  1752  ax11ev  1753  equs5or  1755  raleqf  2553  alexeq  2733  mo2icl  2784  sbc19.21g  2895  csbiebg  2958  ralss  3073  ssuni  3652  intmin4  3693  ssexg  3946  pocl  4097  frforeq1  4137  frforeq2  4139  frind  4146  ontr2exmid  4307  elirr  4323  en2lp  4336  tfisi  4368  vtoclr  4447  sosng  4472  fun11  5037  funimass4  5303  dff13  5490  f1mpt  5493  isopolem  5543  oprabid  5619  caovcan  5747  caoftrn  5818  dfsmo2  5987  tfr1onlemsucfn  6040  tfr1onlemsucaccv  6041  tfr1onlembxssdm  6043  tfr1onlembfn  6044  tfr1onlemres  6049  tfrcllemsucfn  6053  tfrcllemsucaccv  6054  tfrcllembxssdm  6056  tfrcllembfn  6057  tfrcllemres  6062  tfrcl  6064  qliftfun  6307  ecoptocl  6312  ecopovtrn  6322  ecopovtrng  6325  dom2lem  6422  ssfiexmid  6525  domfiexmid  6527  findcard  6537  findcard2  6538  findcard2s  6539  supmoti  6609  eqsupti  6612  suplubti  6616  supisoex  6625  isomnimap  6714  ltsonq  6878  prarloclem3  6977  lttrsr  7229  mulextsr1  7247  axpre-lttrn  7340  axpre-mulext  7344  axcaucvglemres  7355  prime  8755  raluz  8975  indstr  8990  supinfneg  8992  infsupneg  8993  fz1sbc  9417  exbtwnzlemshrink  9563  rebtwn2zlemshrink  9568  caucvgre  10255  maxleast  10487  rexanre  10494  rexico  10495  minmax  10500  addcn2  10537  mulcn2  10539  cn1lem  10540  zsupcllemstep  10735  zsupcllemex  10736  bezoutlemmain  10781  dfgcd2  10797  exprmfct  10913  prmdvdsexpr  10923  sqrt2irr  10935  pw2dvdslemn  10937  bj-rspgt  11043  bdssexg  11152
  Copyright terms: Public domain W3C validator