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  2851  alexeq  2865  mo2icl  2918  sbc19.21g  3033  csbcow  3070  csbiebg  3101  ralss  3223  ifmdc  3576  ssuni  3833  intmin4  3874  ssexg  4144  pocl  4305  frforeq1  4345  frforeq2  4347  frind  4354  ontr2exmid  4526  elirr  4542  en2lp  4555  tfisi  4588  vtoclr  4676  sosng  4701  fun11  5285  funimass4  5568  dff13  5771  f1mpt  5774  isopolem  5825  oprabid  5909  caovcan  6041  caoftrn  6110  dfsmo2  6290  tfr1onlemsucfn  6343  tfr1onlemsucaccv  6344  tfr1onlembxssdm  6346  tfr1onlembfn  6347  tfr1onlemres  6352  tfrcllemsucfn  6356  tfrcllemsucaccv  6357  tfrcllembxssdm  6359  tfrcllembfn  6360  tfrcllemres  6365  tfrcl  6367  qliftfun  6619  ecoptocl  6624  ecopovtrn  6634  ecopovtrng  6637  dom2lem  6774  ssfiexmid  6878  domfiexmid  6880  findcard  6890  findcard2  6891  findcard2s  6892  fiintim  6930  supmoti  6994  eqsupti  6997  suplubti  7001  supisoex  7010  isomnimap  7137  ismkvmap  7154  iswomnimap  7166  tapeq1  7253  ltsonq  7399  prarloclem3  7498  suplocexpr  7726  lttrsr  7763  mulextsr1  7782  suplocsrlem  7809  axpre-lttrn  7885  axpre-mulext  7889  axcaucvglemres  7900  axpre-suploclemres  7902  axpre-suploc  7903  prime  9354  raluz  9580  indstr  9595  supinfneg  9597  infsupneg  9598  fz1sbc  10098  exbtwnzlemshrink  10251  rebtwn2zlemshrink  10256  apexp1  10700  zfz1iso  10823  caucvgre  10992  maxleast  11224  rexanre  11231  rexico  11232  minmax  11240  xrminmax  11275  addcn2  11320  mulcn2  11322  cn1lem  11324  zsupcllemstep  11948  zsupcllemex  11949  zsupssdc  11957  bezoutlemmain  12001  dfgcd2  12017  exprmfct  12140  prmdvdsexpr  12152  sqrt2irr  12164  pw2dvdslemn  12167  prmpwdvds  12355  infpn2  12459  istopg  13538  lmbr  13752  metcnp  14051  addcncntoplem  14090  lgseisenlem2  14490  2sqlem6  14506  2sqlem8  14509  2sqlem10  14511  bj-rspgt  14577  bdssexg  14695  strcollnft  14775  sscoll2  14779