Theorem imbi1d 341

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 248	. . 3 ⊢ (𝜑 → (𝜒 → 𝜓))
3	2	imim1d 82	. 2 ⊢ (𝜑 → ((𝜓 → 𝜃) → (𝜒 → 𝜃)))
4	1	biimpd 229	. . 3 ⊢ (𝜑 → (𝜓 → 𝜒))
5	4	imim1d 82	. 2 ⊢ (𝜑 → ((𝜒 → 𝜃) → (𝜓 → 𝜃)))
6	3, 5	impbid 212	1 ⊢ (𝜑 → ((𝜓 → 𝜃) ↔ (𝜒 → 𝜃)))

Syntax hints:   → wi 4   ↔ wb 206

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 207

This theorem is referenced by:  imbi12d  344  imbi1  347  imim21b  394  pm5.33  835  con3ALT  1084  norasslem3  1536  sbjust  2064  sbequ  2084  sb6  2086  19.21t  2207  sb4b  2473  drsb1  2493  cbvralsvw  3287  sbralie  3323  raleqf  3326  ralcom2  3348  rmoeq1  3384  rspceaimv  3591  ralxpxfr2d  3609  alexeqg  3614  elab6g  3632  mo2icl  3682  sbc19.21g  3822  csbiebg  3891  ralss  4018  ralssOLD  4020  r19.37zv  4461  reuprg0  4662  unissb  4899  intmin4  4937  dftr2c  5212  ssexg  5273  pocl  5547  vtoclr  5694  frsn  5719  cotrg  6069  dffun2  6509  fun11  6574  funimass4  6907  dff13  7211  f1mpt  7218  isopolem  7302  fnssintima  7319  oprabidw  7400  oprabid  7401  caovcan  7573  imaeqalov  7608  caoftrn  7674  ordunisuc2  7800  tfisi  7815  tfinds  7816  tfindsg  7817  tfindsg2  7818  dfom2  7824  findsg  7853  frxp  8082  xpord2indlem  8103  xpord3inddlem  8110  poseq  8114  frrlem12  8253  dfsmo2  8293  qliftfun  8752  ecoptocl  8757  ecopovtrn  8770  dom2lem  8940  findcard  9104  findcard2  9105  ssfi  9114  findcard3  9205  findcard3OLD  9206  fiint  9253  fiintOLD  9254  supmo  9379  eqsup  9383  suplub  9387  supisoex  9402  infmo  9424  wemaplem1  9475  wemaplem2  9476  wemapsolem  9479  oemapvali  9613  cantnf  9622  wemapwe  9626  ttrclss  9649  karden  9824  aceq1  10046  zorn2lem1  10425  axrepndlem2  10522  axregndlem2  10532  gruurn  10727  indpi  10836  nqereu  10858  prcdnq  10922  supexpr  10983  ltsosr  11023  supsrlem  11040  supsr  11041  axpre-lttrn  11095  axpre-sup  11098  prodgt0  12005  infm3  12118  prime  12591  raluz  12831  zsupss  12872  uzsupss  12875  xrsupsslem  13243  xrinfmsslem  13244  fz1sbc  13537  ssnn0fi  13926  fi1uzind  14448  brfi1indALT  14451  wrdind  14663  wrd2ind  14664  relexprelg  14980  rtrclreclem3  15002  relexpindlem  15005  relexpind  15006  rtrclind  15007  rexanre  15289  rexico  15296  reusq0  15407  limsupgle  15419  ello12  15458  ello12r  15459  ello1d  15465  elo12  15469  elo12r  15470  lo1resb  15506  o1resb  15508  rlimcn3  15532  addcn2  15536  mulcn2  15538  lo1le  15594  rpnnen2lem12  16169  sqrt2irr  16193  dfgcd2  16492  exprmfct  16650  isprm5  16653  isprm7  16654  prmdvdsexpr  16663  prmpwdvds  16851  vdwmc2  16926  ramtlecl  16947  ramub  16960  rami  16962  ramcl  16976  firest  17371  mreexexd  17585  acsfn  17596  prslem  18234  ispos  18251  posi  18254  isposd  18259  pospropd  18262  lubeldm  18288  lubval  18291  glbeldm  18301  glbval  18304  joinval2lem  18315  meetval2lem  18329  odlem1  19441  mndodcongi  19449  gexlem1  19485  sylow1lem3  19506  efgredlemb  19652  efgred  19654  frgpnabllem1  19779  isrrg  20583  isdomn4  20601  domnlcanb  20605  domnrcanb  20607  acsfn1p  20684  xrsdsreclb  21306  islindf4  21723  mplsubglem  21884  mpllsslem  21885  ltbval  21926  opsrval  21929  psdmul  22029  mdetunilem1  22475  mdetunilem3  22477  mdetunilem4  22478  mdetunilem9  22483  chpscmat  22705  istopg  22758  isclo2  22951  neiptoptop  22994  neiptopnei  22995  lmbr  23121  ist0  23183  ist1-2  23210  t1sep2  23232  cmpfi  23271  2ndcdisj  23319  1stccn  23326  iskgen3  23412  ptpjopn  23475  hausdiag  23508  xkopt  23518  ist0-4  23592  isr0  23600  r0sep  23611  fbfinnfr  23704  fmfnfmlem2  23818  fmfnfmlem4  23820  fmfnfm  23821  cnflf  23865  cnfcf  23905  tmdgsum2  23959  tsmsf1o  24008  tsmsxplem1  24016  ustssel  24069  ustincl  24071  ustdiag  24072  ustinvel  24073  ustexhalf  24074  ust0  24083  ustuqtop4  24108  utopsnneiplem  24111  isucn2  24142  iducn  24146  metcnp  24405  txmetcnp  24411  metucn  24435  ngptgp  24500  nlmvscnlem1  24550  xrge0tsms  24699  xmetdcn2  24702  addcnlem  24729  ipcnlem1  25121  caucfil  25159  metcld  25182  metcld2  25183  ellimc2  25754  dvne0  25892  mdegleb  25945  mdegle0  25958  ply1divex  26018  fta1g  26051  dgrco  26157  plydivex  26181  fta1  26192  vieta1  26196  cxpcn3lem  26633  rlimcnp  26851  mpodvdsmulf1o  27080  dvdsmulf1o  27082  ppiublem1  27089  dchrinv  27148  lgseisenlem2  27263  2sqlem6  27310  2sqlem8  27313  2sqlem10  27315  nocvxminlem  27665  addsprop  27859  sleadd1  27872  negsprop  27917  mulsprop  28009  bdayon  28149  onsfi  28223  expsne0  28297  istrkgc  28357  istrkgb  28358  axtgcgrid  28366  axtg5seg  28368  axtgpasch  28370  axtgeucl  28375  tgcgr4  28434  axlowdimlem15  28859  usgr2wlkneq  29659  usgr2pthlem  29666  friendshipgt3  30300  isnvlem  30512  vacn  30596  smcnlem  30599  norm3lemt  31054  isch2  31125  chlimi  31136  omlsii  31305  eigorth  31740  stcltr1i  32176  elat2  32242  funcnv5mpt  32565  xrge0infss  32656  sgn3da  32732  sgnnbi  32736  sgnpbi  32737  wrdt2ind  32848  resspos  32865  xrge0tsmsd  32975  elrgspnlem4  33169  domnlcanOLD  33203  islinds5  33311  islbs5  33324  prmidlval  33381  rprmdvdspow  33477  1arithufdlem3  33490  evl1deg1  33518  evl1deg2  33519  evl1deg3  33520  ply1dg1rt  33521  ist0cld  33796  qqhucn  33955  esum2d  34056  eulerpartlemgvv  34340  tgoldbachgt  34627  axtgupdim2ALTV  34632  bnj1145  34956  bnj1171  34963  bnj1172  34964  isacycgr1  35106  acycgrcycl  35107  erdszelem8  35158  satfrnmapom  35330  mclsval  35523  mclsax  35529  mclsppslem  35543  climuzcnv  35631  elintfv  35725  ifscgr  36005  idinside  36045  brsegle  36069  ixpeq12dv  36177  trer  36277  filnetlem4  36342  bj-ssblem1  36615  bj-ssblem2  36616  bj-ax12  36618  bj-19.21t0  36791  mobidvALT  36818  currysetlem  36906  currysetlem1  36908  wl-ax12v2cl  37467  wl-sbrimt  37508  fin2so  37574  ptrecube  37587  poimirlem26  37613  poimirlem27  37614  heicant  37622  mbfresfi  37633  itg2addnc  37641  filbcmb  37707  sdclem2  37709  fdc  37712  fdc1  37713  rngoidmlem  37903  divrngidl  37995  pridlval  38000  smprngopr  38019  inecmo  38310  elcnvrefrels3  38499  disjlem18  38765  ax12inda  38914  ax12v2-o  38915  isat3  39273  iscvlat2N  39290  psubspset  39711  ldilfset  40075  ldilset  40076  dilfsetN  40119  dilsetN  40120  cdlemefrs29bpre0  40363  cdlemefrs29clN  40366  cdlemefrs32fva  40367  cdlemn11pre  41177  dihord2pre  41192  lpolsetN  41449  isprimroot  42054  primrootsunit1  42058  primrootscoprbij  42063  aks6d1c1  42077  hashscontpow  42083  sticksstones11  42117  sticksstones12a  42118  aks6d1c6lem3  42133  fimgmcyc  42495  fsuppind  42551  aomclem8  43023  hbtlem5  43090  unielss  43180  ifpbi1  43439  ifpbi12  43450  ifpbi13  43451  ntrneik2  44054  ntrneikb  44056  gneispacess2  44108  2sbc6g  44377  sbiota1  44396  relpeq2  44908  nregmodel  44980  uzwo4  45020  iineq12dv  45073  fsumiunss  45546  limsupre  45612  limsupref  45656  limsupbnd1f  45657  limsupmnf  45692  limsupre2  45696  limsupmnfuzlem  45697  limsupre2mpt  45701  limsupre3  45704  limsupre3mpt  45705  ioodvbdlimc1lem2  45903  ioodvbdlimc2lem  45905  dvmptfprodlem  45915  wallispilem3  46038  fourierdlem48  46125  sge0f1o  46353  sge0iunmptlemre  46386  sge0iunmpt  46389  vonioo  46653  vonicc  46656  fcoresf1  47043  2reu8i  47087  2reuimp0  47088  2reuimp  47089  sprsymrelfolem2  47467  paireqne  47485  nfermltlrev  47718  bgoldbachlt  47787  tgoldbachlt  47790  gpgedgiov  48029  gpgedg2ov  48030  gpgedg2iv  48031  pgnbgreunbgrlem1  48076  pgnbgreunbgrlem3  48081  pgnbgreunbgrlem4  48082  pgnbgreunbgrlem6  48087  pgnbgreunbgr  48088  ply1mulgsumlem1  48348  ply1mulgsumlem2  48349  elbigo2  48514  elbigo2r  48515  logic1  48752  postcposALT  49530  postc  49531  setrecseq  49647  setrec1lem1  49649  aacllem  49763