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  609  imordc  897  drsb1  1799  ax11v2  1820  ax11v  1827  ax11ev  1828  equs5or  1830  cbvabw  2300  raleqf  2669  rspceaimv  2850  alexeq  2864  mo2icl  2917  sbc19.21g  3032  csbcow  3069  csbiebg  3100  ralss  3222  ifmdc  3575  ssuni  3832  intmin4  3873  ssexg  4143  pocl  4304  frforeq1  4344  frforeq2  4346  frind  4353  ontr2exmid  4525  elirr  4541  en2lp  4554  tfisi  4587  vtoclr  4675  sosng  4700  fun11  5284  funimass4  5567  dff13  5769  f1mpt  5772  isopolem  5823  oprabid  5907  caovcan  6039  caoftrn  6108  dfsmo2  6288  tfr1onlemsucfn  6341  tfr1onlemsucaccv  6342  tfr1onlembxssdm  6344  tfr1onlembfn  6345  tfr1onlemres  6350  tfrcllemsucfn  6354  tfrcllemsucaccv  6355  tfrcllembxssdm  6357  tfrcllembfn  6358  tfrcllemres  6363  tfrcl  6365  qliftfun  6617  ecoptocl  6622  ecopovtrn  6632  ecopovtrng  6635  dom2lem  6772  ssfiexmid  6876  domfiexmid  6878  findcard  6888  findcard2  6889  findcard2s  6890  fiintim  6928  supmoti  6992  eqsupti  6995  suplubti  6999  supisoex  7008  isomnimap  7135  ismkvmap  7152  iswomnimap  7164  tapeq1  7251  ltsonq  7397  prarloclem3  7496  suplocexpr  7724  lttrsr  7761  mulextsr1  7780  suplocsrlem  7807  axpre-lttrn  7883  axpre-mulext  7887  axcaucvglemres  7898  axpre-suploclemres  7900  axpre-suploc  7901  prime  9352  raluz  9578  indstr  9593  supinfneg  9595  infsupneg  9596  fz1sbc  10096  exbtwnzlemshrink  10249  rebtwn2zlemshrink  10254  apexp1  10698  zfz1iso  10821  caucvgre  10990  maxleast  11222  rexanre  11229  rexico  11230  minmax  11238  xrminmax  11273  addcn2  11318  mulcn2  11320  cn1lem  11322  zsupcllemstep  11946  zsupcllemex  11947  zsupssdc  11955  bezoutlemmain  11999  dfgcd2  12015  exprmfct  12138  prmdvdsexpr  12150  sqrt2irr  12162  pw2dvdslemn  12165  prmpwdvds  12353  infpn2  12457  istopg  13502  lmbr  13716  metcnp  14015  addcncntoplem  14054  lgseisenlem2  14454  2sqlem6  14470  2sqlem8  14473  2sqlem10  14475  bj-rspgt  14541  bdssexg  14659  strcollnft  14739  sscoll2  14743