Theorem imbi1d 230

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 157	. . 3 ⊢ (𝜑 → (𝜒 → 𝜓))
3	2	imim1d 75	. 2 ⊢ (𝜑 → ((𝜓 → 𝜃) → (𝜒 → 𝜃)))
4	1	biimpd 143	. . 3 ⊢ (𝜑 → (𝜓 → 𝜒))
5	4	imim1d 75	. 2 ⊢ (𝜑 → ((𝜒 → 𝜃) → (𝜓 → 𝜃)))
6	3, 5	impbid 128	1 ⊢ (𝜑 → ((𝜓 → 𝜃) ↔ (𝜒 → 𝜃)))

Syntax hints:   → wi 4   ↔ wb 104

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  imbi12d  233  imbi1  235  imim21b  251  pm5.33  598  imordc  882  drsb1  1771  ax11v2  1792  ax11v  1799  ax11ev  1800  equs5or  1802  raleqf  2622  rspceaimv  2797  alexeq  2811  mo2icl  2863  sbc19.21g  2977  csbiebg  3042  ralss  3163  ifmdc  3509  ssuni  3758  intmin4  3799  ssexg  4067  pocl  4225  frforeq1  4265  frforeq2  4267  frind  4274  ontr2exmid  4440  elirr  4456  en2lp  4469  tfisi  4501  vtoclr  4587  sosng  4612  fun11  5190  funimass4  5472  dff13  5669  f1mpt  5672  isopolem  5723  oprabid  5803  caovcan  5935  caoftrn  6007  dfsmo2  6184  tfr1onlemsucfn  6237  tfr1onlemsucaccv  6238  tfr1onlembxssdm  6240  tfr1onlembfn  6241  tfr1onlemres  6246  tfrcllemsucfn  6250  tfrcllemsucaccv  6251  tfrcllembxssdm  6253  tfrcllembfn  6254  tfrcllemres  6259  tfrcl  6261  qliftfun  6511  ecoptocl  6516  ecopovtrn  6526  ecopovtrng  6529  dom2lem  6666  ssfiexmid  6770  domfiexmid  6772  findcard  6782  findcard2  6783  findcard2s  6784  fiintim  6817  supmoti  6880  eqsupti  6883  suplubti  6887  supisoex  6896  isomnimap  7009  ismkvmap  7028  ltsonq  7206  prarloclem3  7305  suplocexpr  7533  lttrsr  7570  mulextsr1  7589  suplocsrlem  7616  axpre-lttrn  7692  axpre-mulext  7696  axcaucvglemres  7707  axpre-suploclemres  7709  axpre-suploc  7710  prime  9150  raluz  9373  indstr  9388  supinfneg  9390  infsupneg  9391  fz1sbc  9876  exbtwnzlemshrink  10026  rebtwn2zlemshrink  10031  zfz1iso  10584  caucvgre  10753  maxleast  10985  rexanre  10992  rexico  10993  minmax  11001  xrminmax  11034  addcn2  11079  mulcn2  11081  cn1lem  11083  zsupcllemstep  11638  zsupcllemex  11639  bezoutlemmain  11686  dfgcd2  11702  exprmfct  11818  prmdvdsexpr  11828  sqrt2irr  11840  pw2dvdslemn  11843  istopg  12166  lmbr  12382  metcnp  12681  addcncntoplem  12720  bj-rspgt  12993  bdssexg  13102