Theorem imbi1d 231

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

Step	Hyp	Ref	Expression
1		imbid.1	. . . 4 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
2	1	biimprd 158	. . 3 ⊢ (𝜑 → (𝜒 → 𝜓))
3	2	imim1d 75	. 2 ⊢ (𝜑 → ((𝜓 → 𝜃) → (𝜒 → 𝜃)))
4	1	biimpd 144	. . 3 ⊢ (𝜑 → (𝜓 → 𝜒))
5	4	imim1d 75	. 2 ⊢ (𝜑 → ((𝜒 → 𝜃) → (𝜓 → 𝜃)))
6	3, 5	impbid 129	1 ⊢ (𝜑 → ((𝜓 → 𝜃) ↔ (𝜒 → 𝜃)))

Syntax hints:   → wi 4   ↔ wb 105

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  imbi12d  234  imbi1  236  imim21b  253  pm5.33  611  imordc  902  drsb1  1845  ax11v2  1866  ax11v  1873  ax11ev  1874  equs5or  1876  cbvabw  2352  raleqf  2724  rspceaimv  2915  alexeq  2929  mo2icl  2982  sbc19.21g  3097  csbcow  3135  csbiebg  3167  ralss  3290  ifmdc  3645  ssuni  3909  intmin4  3950  ssexg  4222  pocl  4393  frforeq1  4433  frforeq2  4435  frind  4442  ontr2exmid  4616  elirr  4632  en2lp  4645  tfisi  4678  vtoclr  4766  sosng  4791  fun11  5387  funimass4  5683  dff13  5891  f1mpt  5894  isopolem  5945  oprabid  6032  caovcan  6169  caoftrn  6249  dfsmo2  6431  tfr1onlemsucfn  6484  tfr1onlemsucaccv  6485  tfr1onlembxssdm  6487  tfr1onlembfn  6488  tfr1onlemres  6493  tfrcllemsucfn  6497  tfrcllemsucaccv  6498  tfrcllembxssdm  6500  tfrcllembfn  6501  tfrcllemres  6506  tfrcl  6508  qliftfun  6762  ecoptocl  6767  ecopovtrn  6777  ecopovtrng  6780  dom2lem  6921  ssfiexmid  7034  domfiexmid  7036  findcard  7046  findcard2  7047  findcard2s  7048  fiintim  7089  supmoti  7156  eqsupti  7159  suplubti  7163  supisoex  7172  isomnimap  7300  ismkvmap  7317  iswomnimap  7329  tapeq1  7434  ltsonq  7581  prarloclem3  7680  suplocexpr  7908  lttrsr  7945  mulextsr1  7964  suplocsrlem  7991  axpre-lttrn  8067  axpre-mulext  8071  axcaucvglemres  8082  axpre-suploclemres  8084  axpre-suploc  8085  prime  9542  raluz  9769  indstr  9784  supinfneg  9786  infsupneg  9787  fz1sbc  10288  zsupcllemstep  10444  zsupcllemex  10445  zsupssdc  10453  exbtwnzlemshrink  10463  rebtwn2zlemshrink  10468  apexp1  10935  zfz1iso  11058  wrdind  11249  wrd2ind  11250  caucvgre  11487  maxleast  11719  rexanre  11726  rexico  11727  minmax  11736  xrminmax  11771  addcn2  11816  mulcn2  11818  cn1lem  11820  bezoutlemmain  12514  dfgcd2  12530  exprmfct  12655  prmdvdsexpr  12667  sqrt2irr  12679  pw2dvdslemn  12682  prmpwdvds  12873  infpn2  13022  isrrg  14221  istopg  14667  lmbr  14881  metcnp  15180  addcncntoplem  15229  mpodvdsmulf1o  15658  lgseisenlem2  15744  2sqlem6  15793  2sqlem8  15796  2sqlem10  15798  bj-rspgt  16108  bdssexg  16225  strcollnft  16305  sscoll2  16309  nnnninfex  16347