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  617  imordc  909  drsb1  1852  ax11v2  1873  ax11v  1880  ax11ev  1881  equs5or  1883  cbvabw  2363  raleqf  2745  rspceaimv  2938  alexeq  2952  mo2icl  3005  sbc19.21g  3120  csbcow  3158  csbiebg  3190  ralss  3314  ifmdc  3680  ssuni  3952  intmin4  3993  ssexg  4267  pocl  4443  frforeq1  4483  frforeq2  4485  frind  4492  ontr2exmid  4667  elirr  4683  en2lp  4696  tfisi  4729  vtoclr  4818  sosng  4843  fun11  5443  funimass4  5747  dff13  5964  f1mpt  5967  isopolem  6018  oprabid  6107  caovcan  6244  caoftrn  6325  dfsmo2  6548  tfr1onlemsucfn  6601  tfr1onlemsucaccv  6602  tfr1onlembxssdm  6604  tfr1onlembfn  6605  tfr1onlemres  6610  tfrcllemsucfn  6614  tfrcllemsucaccv  6615  tfrcllembxssdm  6617  tfrcllembfn  6618  tfrcllemres  6623  tfrcl  6625  qliftfun  6881  ecoptocl  6886  ecopovtrn  6896  ecopovtrng  6899  dom2lem  7048  ssfiexmid  7168  ssfiexmidt  7170  domfiexmid  7172  findcard  7182  findcard2  7183  findcard2s  7184  fiintim  7228  supmoti  7323  eqsupti  7326  suplubti  7330  supisoex  7339  isomnimap  7467  ismkvmap  7484  iswomnimap  7496  tapeq1  7608  ltsonq  7755  prarloclem3  7854  suplocexpr  8082  lttrsr  8119  mulextsr1  8138  suplocsrlem  8165  axpre-lttrn  8241  axpre-mulext  8245  axcaucvglemres  8256  axpre-suploclemres  8258  axpre-suploc  8259  prime  9724  raluz  9957  indstr  9972  supinfneg  9974  infsupneg  9975  fz1sbc  10481  zsupcllemstep  10640  zsupcllemex  10641  zsupssdc  10651  exbtwnzlemshrink  10661  rebtwn2zlemshrink  10666  apexp1  11134  zfz1iso  11271  wrdind  11472  wrd2ind  11473  caucvgre  11725  maxleast  11957  rexanre  11964  rexico  11965  minmax  11974  xrminmax  12009  addcn2  12054  mulcn2  12056  cn1lem  12058  bezoutlemmain  12753  dfgcd2  12769  exprmfct  12894  prmdvdsexpr  12906  sqrt2irr  12918  pw2dvdslemn  12921  prmpwdvds  13112  infpn2  13325  isrrg  14544  opprdrng  14593  istopg  15023  lmbr  15237  metcnp  15536  addcncntoplem  15585  mpodvdsmulf1o  16018  lgseisenlem2  16104  2sqlem6  16153  2sqlem8  16156  2sqlem10  16158  bj-rspgt  16728  bdssexg  16844  strcollnft  16924  sscoll2  16928  exmidcon  16950  exmidpeirce  16951  nnnninfex  16970