Theorem imbi1d 342

Description: Deduction adding a consequent to both sides of a logical equivalence. (Contributed by NM, 11-May-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 249	. . 3 ⊢ (𝜑 → (𝜒 → 𝜓))
3	2	imim1d 82	. 2 ⊢ (𝜑 → ((𝜓 → 𝜃) → (𝜒 → 𝜃)))
4	1	biimpd 230	. . 3 ⊢ (𝜑 → (𝜓 → 𝜒))
5	4	imim1d 82	. 2 ⊢ (𝜑 → ((𝜒 → 𝜃) → (𝜓 → 𝜃)))
6	3, 5	impbid 213	1 ⊢ (𝜑 → ((𝜓 → 𝜃) ↔ (𝜒 → 𝜃)))

Syntax hints:   → wi 4   ↔ wb 207

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 208

This theorem is referenced by:  imbi12d  345  imbi1  348  imim21b  395  pm5.33  841  con3ALT  1090  norasslem3  1543  sbjust  2072  sbequ  2094  sb6  2096  19.21t  2218  sb4b  2483  drsb1  2503  cbvralsvw  3290  sbralie  3317  raleqf  3320  ralcom2  3341  rmoeq1  3375  rspceaimv  3566  ralxpxfr2d  3584  alexeqg  3589  elab6g  3607  mo2icl  3655  sbc19.21g  3794  csbiebg  3863  ralss  3987  ralssOLD  3989  r19.37zv  4435  reuprg0  4634  unissb  4871  intmin4  4907  dftr2c  5182  ssexg  5251  pocl  5534  vtoclr  5681  frsn  5706  cotrg  6061  dffun2  6495  fun11  6559  funimass4  6891  dff13  7198  f1mpt  7205  isopolem  7289  fnssintima  7306  oprabidw  7387  oprabid  7388  caovcan  7560  imaeqalov  7595  caoftrn  7661  ordunisuc2  7784  tfisi  7799  tfinds  7800  tfindsg  7801  tfindsg2  7802  dfom2  7808  findsg  7837  frxp  8066  xpord2indlem  8087  xpord3inddlem  8094  poseq  8098  frrlem12  8237  dfsmo2  8277  qliftfun  8739  ecoptocl  8744  ecopovtrn  8757  dom2lem  8929  findcard  9088  findcard2  9089  ssfi  9097  findcard3  9183  fiint  9227  supmo  9355  eqsup  9359  suplub  9363  supisoex  9378  infmo  9400  wemaplem1  9451  wemaplem2  9452  wemapsolem  9455  oemapvali  9596  cantnf  9605  wemapwe  9609  ttrclss  9632  karden  9810  aceq1  10030  zorn2lem1  10409  axrepndlem2  10507  axregndlem2  10517  gruurn  10712  indpi  10821  nqereu  10843  prcdnq  10907  supexpr  10968  ltsosr  11008  supsrlem  11025  supsr  11026  axpre-lttrn  11080  axpre-sup  11083  prodgt0  11993  infm3  12106  prime  12601  raluz  12837  zsupss  12878  uzsupss  12881  xrsupsslem  13250  xrinfmsslem  13251  fz1sbc  13545  ssnn0fi  13938  fi1uzind  14460  brfi1indALT  14463  wrdind  14675  wrd2ind  14676  relexprelg  14991  rtrclreclem3  15013  relexpindlem  15016  relexpind  15017  rtrclind  15018  rexanre  15300  rexico  15307  reusq0  15418  limsupgle  15430  ello12  15469  ello12r  15470  ello1d  15476  elo12  15480  elo12r  15481  lo1resb  15517  o1resb  15519  rlimcn3  15543  addcn2  15547  mulcn2  15549  lo1le  15605  rpnnen2lem12  16183  sqrt2irr  16207  dfgcd2  16506  exprmfct  16665  isprm5  16668  isprm7  16669  prmdvdsexpr  16678  prmpwdvds  16866  vdwmc2  16941  ramtlecl  16962  ramub  16975  rami  16977  ramcl  16991  firest  17386  mreexexd  17605  acsfn  17616  prslem  18254  ispos  18271  posi  18274  isposd  18279  pospropd  18282  lubeldm  18308  lubval  18311  glbeldm  18321  glbval  18324  joinval2lem  18335  meetval2lem  18349  resspos  18386  odlem1  19501  mndodcongi  19509  gexlem1  19545  sylow1lem3  19566  efgredlemb  19712  efgred  19714  frgpnabllem1  19839  isrrg  20670  isdomn4  20688  domnlcanb  20692  domnrcanb  20694  acsfn1p  20771  xrsdsreclb  21389  islindf4  21813  mplsubglem  21973  mpllsslem  21974  ltbval  22019  opsrval  22022  psdmul  22154  mdetunilem1  22595  mdetunilem3  22597  mdetunilem4  22598  mdetunilem9  22603  chpscmat  22825  istopg  22878  isclo2  23071  neiptoptop  23114  neiptopnei  23115  lmbr  23241  ist0  23303  ist1-2  23330  t1sep2  23352  cmpfi  23391  2ndcdisj  23439  1stccn  23446  iskgen3  23532  ptpjopn  23595  hausdiag  23628  xkopt  23638  ist0-4  23712  isr0  23720  r0sep  23731  fbfinnfr  23824  fmfnfmlem2  23938  fmfnfmlem4  23940  fmfnfm  23941  cnflf  23985  cnfcf  24025  tmdgsum2  24079  tsmsf1o  24128  tsmsxplem1  24136  ustssel  24189  ustincl  24191  ustdiag  24192  ustinvel  24193  ustexhalf  24194  ust0  24203  ustuqtop4  24227  utopsnneiplem  24230  isucn2  24261  iducn  24265  metcnp  24524  txmetcnp  24530  metucn  24554  ngptgp  24619  nlmvscnlem1  24669  xrge0tsms  24818  xmetdcn2  24821  addcnlem  24848  ipcnlem1  25230  caucfil  25268  metcld  25291  metcld2  25292  ellimc2  25862  dvne0  25996  mdegleb  26047  mdegle0  26060  ply1divex  26120  fta1g  26153  dgrco  26258  plydivex  26281  fta1  26292  vieta1  26296  cxpcn3lem  26729  rlimcnp  26947  mpodvdsmulf1o  27175  dvdsmulf1o  27177  ppiublem1  27183  dchrinv  27242  lgseisenlem2  27357  2sqlem6  27404  2sqlem8  27407  2sqlem10  27409  nocvxminlem  27764  addsprop  27986  leadds1  27999  negsprop  28045  mulsprop  28140  bdayons  28286  onsfi  28366  expsne0  28446  istrkgc  28540  istrkgb  28541  axtgcgrid  28549  axtg5seg  28551  axtgpasch  28553  axtgeucl  28558  tgcgr4  28617  axlowdimlem15  29043  usgr2wlkneq  29842  usgr2pthlem  29849  friendshipgt3  30486  isnvlem  30699  vacn  30783  smcnlem  30786  norm3lemt  31241  isch2  31312  chlimi  31323  omlsii  31492  eigorth  31927  stcltr1i  32363  elat2  32429  funcnv5mpt  32759  xrge0infss  32852  sgn3da  32926  sgnnbi  32930  sgnpbi  32931  wrdt2ind  33032  xrge0tsmsd  33154  elrgspnlem4  33326  domnlcanOLD  33361  islinds5  33450  islbs5  33463  prmidlval  33520  rprmdvdspow  33616  1arithufdlem3  33629  evl1deg1  33659  evl1deg2  33660  evl1deg3  33661  ply1dg1rt  33663  ist0cld  34017  qqhucn  34176  esum2d  34277  eulerpartlemgvv  34560  tgoldbachgt  34847  axtgupdim2ALTV  34852  bnj1145  35175  bnj1171  35182  bnj1172  35183  tz9.1regs  35315  isacycgr1  35374  acycgrcycl  35375  erdszelem8  35426  satfrnmapom  35598  mclsval  35791  mclsax  35797  mclsppslem  35811  climuzcnv  35899  elintfv  35993  ifscgr  36272  idinside  36312  brsegle  36336  ixpeq12dv  36444  trer  36544  filnetlem4  36609  axtcond  36706  axuntco  36707  dfttc4lem1  36756  mh-setindnd  36765  mh-unprimbi  36772  mh-regprimbi  36773  mh-infprim2bi  36775  bj-ssblem1  36994  bj-ssblem2  36995  bj-ax12  36997  bj-19.21t0  37183  mobidvALT  37210  currysetlem  37298  currysetlem1  37300  wl-ax12v2cl  37868  wl-sbrimt  37918  fin2so  37974  ptrecube  37987  poimirlem26  38013  poimirlem27  38014  heicant  38022  mbfresfi  38033  itg2addnc  38041  filbcmb  38107  sdclem2  38109  fdc  38112  fdc1  38113  rngoidmlem  38303  divrngidl  38395  pridlval  38400  smprngopr  38419  inecmo  38722  elcnvrefrels3  38982  eldisjdmqsim2  39183  qmapeldisjsim  39227  rnqmapeleldisjsim  39229  disjlem18  39270  ax12inda  39440  ax12v2-o  39441  isat3  39799  iscvlat2N  39816  psubspset  40236  ldilfset  40600  ldilset  40601  dilfsetN  40644  dilsetN  40645  cdlemefrs29bpre0  40888  cdlemefrs29clN  40891  cdlemefrs32fva  40892  cdlemn11pre  41702  dihord2pre  41717  lpolsetN  41974  isprimroot  42578  primrootsunit1  42582  primrootscoprbij  42587  aks6d1c1  42601  hashscontpow  42607  sticksstones11  42641  sticksstones12a  42642  aks6d1c6lem3  42657  fimgmcyc  43020  fsuppind  43040  aomclem8  43506  hbtlem5  43573  unielss  43663  ifpbi1  43921  ifpbi12  43932  ifpbi13  43933  ntrneik2  44536  ntrneikb  44538  gneispacess2  44590  2sbc6g  44859  sbiota1  44878  relpeq2  45389  nregmodel  45461  uzwo4  45501  iineq12dv  45553  fsumiunss  46020  limsupre  46084  limsupref  46128  limsupbnd1f  46129  limsupmnf  46164  limsupre2  46168  limsupmnfuzlem  46169  limsupre2mpt  46173  limsupre3  46176  limsupre3mpt  46177  ioodvbdlimc1lem2  46375  ioodvbdlimc2lem  46377  dvmptfprodlem  46387  wallispilem3  46510  fourierdlem48  46597  sge0f1o  46825  sge0iunmptlemre  46858  sge0iunmpt  46861  vonioo  47125  vonicc  47128  fcoresf1  47532  2reu8i  47576  2reuimp0  47577  2reuimp  47578  sprsymrelfolem2  47968  paireqne  47986  nfermltlrev  48235  bgoldbachlt  48304  tgoldbachlt  48307  gpgedgiov  48556  gpgedg2ov  48557  gpgedg2iv  48558  pgnbgreunbgrlem1  48604  pgnbgreunbgrlem3  48609  pgnbgreunbgrlem4  48610  pgnbgreunbgrlem6  48615  pgnbgreunbgr  48616  ply1mulgsumlem1  48877  ply1mulgsumlem2  48878  elbigo2  49043  elbigo2r  49044  logic1  49281  postcposALT  50058  postc  50059  setrecseq  50175  setrec1lem1  50177  aacllem  50291