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  2668  rspceaimv  2849  alexeq  2863  mo2icl  2916  sbc19.21g  3031  csbcow  3068  csbiebg  3099  ralss  3221  ifmdc  3574  ssuni  3831  intmin4  3872  ssexg  4142  pocl  4303  frforeq1  4343  frforeq2  4345  frind  4352  ontr2exmid  4524  elirr  4540  en2lp  4553  tfisi  4586  vtoclr  4674  sosng  4699  fun11  5283  funimass4  5566  dff13  5768  f1mpt  5771  isopolem  5822  oprabid  5906  caovcan  6038  caoftrn  6107  dfsmo2  6287  tfr1onlemsucfn  6340  tfr1onlemsucaccv  6341  tfr1onlembxssdm  6343  tfr1onlembfn  6344  tfr1onlemres  6349  tfrcllemsucfn  6353  tfrcllemsucaccv  6354  tfrcllembxssdm  6356  tfrcllembfn  6357  tfrcllemres  6362  tfrcl  6364  qliftfun  6616  ecoptocl  6621  ecopovtrn  6631  ecopovtrng  6634  dom2lem  6771  ssfiexmid  6875  domfiexmid  6877  findcard  6887  findcard2  6888  findcard2s  6889  fiintim  6927  supmoti  6991  eqsupti  6994  suplubti  6998  supisoex  7007  isomnimap  7134  ismkvmap  7151  iswomnimap  7163  tapeq1  7250  ltsonq  7396  prarloclem3  7495  suplocexpr  7723  lttrsr  7760  mulextsr1  7779  suplocsrlem  7806  axpre-lttrn  7882  axpre-mulext  7886  axcaucvglemres  7897  axpre-suploclemres  7899  axpre-suploc  7900  prime  9351  raluz  9577  indstr  9592  supinfneg  9594  infsupneg  9595  fz1sbc  10095  exbtwnzlemshrink  10248  rebtwn2zlemshrink  10253  apexp1  10697  zfz1iso  10820  caucvgre  10989  maxleast  11221  rexanre  11228  rexico  11229  minmax  11237  xrminmax  11272  addcn2  11317  mulcn2  11319  cn1lem  11321  zsupcllemstep  11945  zsupcllemex  11946  zsupssdc  11954  bezoutlemmain  11998  dfgcd2  12014  exprmfct  12137  prmdvdsexpr  12149  sqrt2irr  12161  pw2dvdslemn  12164  prmpwdvds  12352  infpn2  12456  istopg  13469  lmbr  13683  metcnp  13982  addcncntoplem  14021  lgseisenlem2  14421  2sqlem6  14437  2sqlem8  14440  2sqlem10  14442  bj-rspgt  14508  bdssexg  14626  strcollnft  14706  sscoll2  14710