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  613  imordc  905  drsb1  1848  ax11v2  1869  ax11v  1876  ax11ev  1877  equs5or  1879  cbvabw  2357  raleqf  2737  rspceaimv  2929  alexeq  2943  mo2icl  2996  sbc19.21g  3111  csbcow  3149  csbiebg  3181  ralss  3304  ifmdc  3665  ssuni  3936  intmin4  3977  ssexg  4249  pocl  4424  frforeq1  4464  frforeq2  4466  frind  4473  ontr2exmid  4647  elirr  4663  en2lp  4676  tfisi  4709  vtoclr  4798  sosng  4823  fun11  5423  funimass4  5727  dff13  5941  f1mpt  5944  isopolem  5995  oprabid  6082  caovcan  6219  caoftrn  6299  dfsmo2  6518  tfr1onlemsucfn  6571  tfr1onlemsucaccv  6572  tfr1onlembxssdm  6574  tfr1onlembfn  6575  tfr1onlemres  6580  tfrcllemsucfn  6584  tfrcllemsucaccv  6585  tfrcllembxssdm  6587  tfrcllembfn  6588  tfrcllemres  6593  tfrcl  6595  qliftfun  6851  ecoptocl  6856  ecopovtrn  6866  ecopovtrng  6869  dom2lem  7011  ssfiexmid  7131  ssfiexmidt  7133  domfiexmid  7135  findcard  7145  findcard2  7146  findcard2s  7147  fiintim  7191  supmoti  7284  eqsupti  7287  suplubti  7291  supisoex  7300  isomnimap  7428  ismkvmap  7445  iswomnimap  7457  tapeq1  7566  ltsonq  7713  prarloclem3  7812  suplocexpr  8040  lttrsr  8077  mulextsr1  8096  suplocsrlem  8123  axpre-lttrn  8199  axpre-mulext  8203  axcaucvglemres  8214  axpre-suploclemres  8216  axpre-suploc  8217  prime  9677  raluz  9910  indstr  9925  supinfneg  9927  infsupneg  9928  fz1sbc  10430  zsupcllemstep  10589  zsupcllemex  10590  zsupssdc  10598  exbtwnzlemshrink  10608  rebtwn2zlemshrink  10613  apexp1  11080  zfz1iso  11213  wrdind  11414  wrd2ind  11415  caucvgre  11666  maxleast  11898  rexanre  11905  rexico  11906  minmax  11915  xrminmax  11950  addcn2  11995  mulcn2  11997  cn1lem  11999  bezoutlemmain  12694  dfgcd2  12710  exprmfct  12835  prmdvdsexpr  12847  sqrt2irr  12859  pw2dvdslemn  12862  prmpwdvds  13053  infpn2  13207  isrrg  14408  istopg  14864  lmbr  15078  metcnp  15377  addcncntoplem  15426  mpodvdsmulf1o  15858  lgseisenlem2  15944  2sqlem6  15993  2sqlem8  15996  2sqlem10  15998  bj-rspgt  16558  bdssexg  16674  strcollnft  16754  sscoll2  16758  exmidcon  16780  exmidpeirce  16781  nnnninfex  16800