Theorem imbi1d 344

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 251	. . 3 ⊢ (𝜑 → (𝜒 → 𝜓))
3	2	imim1d 83	. 2 ⊢ (𝜑 → ((𝜓 → 𝜃) → (𝜒 → 𝜃)))
4	1	biimpd 232	. . 3 ⊢ (𝜑 → (𝜓 → 𝜒))
5	4	imim1d 83	. 2 ⊢ (𝜑 → ((𝜒 → 𝜃) → (𝜓 → 𝜃)))
6	3, 5	impbid 215	1 ⊢ (𝜑 → ((𝜓 → 𝜃) ↔ (𝜒 → 𝜃)))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  imbi12d  347  imbi1  350  imim21b  400  pm5.33  849  con3ALT  1101  norasslem3  1566  sbjust  2098  sbequ  2120  sb6  2122  19.21t  2243  sb4b  2505  drsb1  2525  cbvralsvw  3314  sbralie  3339  raleqf  3342  ralcom2  3363  rmoeq1  3397  rspceaimv  3583  ralxpxfr2d  3600  alexeqg  3605  elab6g  3623  mo2icl  3672  sbc19.21g  3810  csbiebg  3879  ralss  4004  ralssOLD  4006  r19.37zv  4463  reuprg0  4663  unissb  4901  intmin4  4937  dftr2c  5215  ssexgOLD  5285  pocl  5567  vtoclr  5714  frsn  5739  cotrg  6105  dffun2  6547  fun11  6612  funimass4  6947  dff13  7256  f1mpt  7263  isopolem  7351  fnssintima  7370  oprabidw  7449  oprabid  7450  caovcan  7623  imaeqalov  7658  caoftrn  7732  ordunisuc2  7853  tfisi  7868  tfinds  7869  tfindsg  7870  tfindsg2  7871  dfom2  7877  findsg  7907  frxp  8136  xpord2indlem  8157  xpord3inddlem  8164  poseq  8168  frrlem12  8308  dfsmo2  8348  qliftfun  8816  ecoptocl  8821  ecopovtrn  8834  dom2lem  9012  findcard  9172  findcard2  9173  ssfi  9181  findcard3  9267  fiint  9311  supmo  9437  eqsup  9441  suplub  9445  supisoex  9460  infmo  9482  wemaplem1  9533  wemaplem2  9534  wemapsolem  9537  oemapvali  9678  cantnf  9687  wemapwe  9691  ttrclss  9714  kardenOLD  9953  setrec1lem1  9959  aceq1  10189  zorn2lem1  10567  axrepndlem2  10671  axregndlem2  10681  gruurn  10876  indpi  10985  nqereu  11007  prcdnq  11071  supexpr  11132  ltsosr  11172  supsrlem  11189  supsr  11190  axpre-lttrn  11244  axpre-sup  11247  prodgt0  12157  infm3  12269  prime  12773  raluz  13016  zsupss  13057  uzsupss  13060  xrsupsslem  13430  xrinfmsslem  13431  fz1sbc  13727  ssnn0fi  14121  fi1uzind  14645  brfi1indALT  14648  wrdind  14864  wrd2ind  14865  relexprelg  15184  rtrclreclem3  15206  relexpindlem  15209  relexpind  15210  rtrclind  15211  sgn3da  15247  sgnnbi  15250  sgnpbi  15251  rexanre  15507  rexico  15514  reusq0  15625  limsupgle  15637  ello12  15676  ello12r  15677  ello1d  15683  elo12  15687  elo12r  15688  lo1resb  15724  o1resb  15726  rlimcn3  15750  addcn2  15754  mulcn2  15756  lo1le  15812  rpnnen2lem12  16386  sqrt2irr  16410  dfgcd2  16712  exprmfct  16873  isprm5  16876  isprm7  16877  prmdvdsexpr  16886  prmpwdvds  17075  vdwmc2  17150  ramtlecl  17171  ramub  17184  rami  17186  ramcl  17200  firest  17596  mreexexd  17815  acsfn  17826  prslem  18464  ispos  18481  posi  18484  isposd  18489  pospropd  18492  lubeldm  18518  lubval  18521  glbeldm  18531  glbval  18534  joinval2lem  18545  meetval2lem  18559  resspos  18596  odlem1  19742  mndodcongi  19750  gexlem1  19786  sylow1lem3  19807  efgredlemb  19953  efgred  19955  frgpnabllem1  20080  isrrg  20943  isdomn4  20960  domnlcanb  20964  domnrcanb  20966  acsfn1p  21049  prmidlval  21611  xrsdsreclb  21713  islindf4  22137  mplsubglem  22299  mpllsslem  22300  ltbval  22345  opsrval  22348  psdmul  22480  mdetunilem1  22920  mdetunilem3  22922  mdetunilem4  22923  mdetunilem9  22928  chpscmat  23153  istopg  23206  isclo2  23399  neiptoptop  23442  neiptopnei  23443  lmbr  23569  ist0  23631  ist1-2  23658  t1sep2  23680  cmpfi  23719  2ndcdisj  23768  1stccn  23775  iskgen3  23861  ptpjopn  23924  hausdiag  23957  xkopt  23967  ist0-4  24041  isr0  24049  r0sep  24060  fbfinnfr  24153  fmfnfmlem2  24267  fmfnfmlem4  24269  fmfnfm  24270  cnflf  24314  cnfcf  24354  tmdgsum2  24408  tsmsf1o  24457  tsmsxplem1  24465  ustssel  24518  ustincl  24520  ustdiag  24521  ustinvel  24522  ustexhalf  24523  ust0  24532  ustuqtop4  24556  utopsnneiplem  24559  isucn2  24590  iducn  24594  metcnp  24853  txmetcnp  24859  metucn  24883  ngptgp  24948  nlmvscnlem1  24998  xrge0tsms  25147  xmetdcn2  25150  addcnlem  25177  ipcnlem1  25559  caucfil  25597  metcld  25620  metcld2  25621  ellimc2  26190  dvne0  26324  mdegleb  26375  mdegle0  26388  ply1divex  26448  fta1g  26481  dgrco  26587  plydivex  26611  fta1  26622  vieta1  26628  cxpcn3lem  27068  rlimcnp  27286  mpodvdsmulf1o  27514  dvdsmulf1o  27516  ppiublem1  27522  dchrinv  27581  lgseisenlem2  27696  2sqlem6  27743  2sqlem8  27746  2sqlem10  27748  nocvxminlem  28133  addsprop  28355  leadds1  28368  negsprop  28414  mulsprop  28509  bdayons  28655  onsfi  28735  expsne0  28815  istrkgc  28909  istrkgb  28910  axtgcgrid  28918  axtg5seg  28920  axtgpasch  28922  axtgeucl  28927  tgcgr4  28987  axlowdimlem15  29527  usgr2wlkneq  30335  usgr2pthlem  30342  isacycgr1  30745  acycgrcycl  30746  friendshipgt3  30992  isnvlem  31205  vacn  31289  smcnlem  31292  norm3lemt  31747  isch2  31818  chlimi  31829  omlsii  31998  eigorth  32433  stcltr1i  32869  elat2  32935  funcnv5mpt  33254  xrge0infss  33345  wrdt2ind  33509  xrge0tsmsd  33627  elrgspnlem4  33799  islinds5  33916  islbs5  33928  rprmdvdspow  34058  1arithufdlem3  34071  evl1deg1  34101  evl1deg2  34102  evl1deg3  34103  ply1dg1rt  34105  ist0cld  34458  qqhucn  34617  esum2d  34718  eulerpartlemgvv  35001  tgoldbachgt  35285  axtgupdim2ALTV  35290  bnj1145  35616  bnj1171  35623  bnj1172  35624  tz9.1regs  35785  erdszelem8  35942  satfrnmapom  36114  mclsval  36307  mclsax  36313  mclsppslem  36327  climuzcnv  36415  elintfv  36509  ifscgr  36789  idinside  36829  brsegle  36853  ixpeq12dv  36985  trer  37084  filnetlem4  37149  axtcond  37246  axuntco  37247  dfttc4lem1  37296  mh-setindnd  37305  mh-unprimbi  37312  mh-regprimbi  37313  mh-infprim2bi  37315  bj-ssblem1  37533  bj-ssblem2  37534  bj-ax12  37536  bj-19.21t0  37722  mobidvALT  37749  currysetlem  37838  currysetlem1  37840  wl-ax12v2cl  38409  wl-sbrimt  38459  fin2so  38510  ptrecube  38518  poimirlem26  38544  poimirlem27  38545  heicant  38553  mbfresfi  38564  itg2addnc  38572  findcard4  38612  filbcmb  38654  sdclem2  38656  fdc  38659  fdc1  38660  rngoidmlem  38850  divrngidl  38942  pridlval  38947  smprngopr  38966  inecmo  39267  elcnvrefrels3  39527  eldisjdmqsim2  39728  qmapeldisjsim  39772  rnqmapeleldisjsim  39774  disjlem18  39815  ax12inda  39985  ax12v2-o  39986  isat3  40344  iscvlat2N  40361  psubspset  40781  ldilfset  41145  ldilset  41146  dilfsetN  41189  dilsetN  41190  cdlemefrs29bpre0  41433  cdlemefrs29clN  41436  cdlemefrs32fva  41437  cdlemn11pre  42247  dihord2pre  42262  lpolsetN  42519  isprimroot  43123  primrootsunit1  43127  primrootscoprbij  43132  aks6d1c1  43146  hashscontpow  43152  sticksstones11  43186  sticksstones12a  43187  aks6d1c6lem3  43202  fimgmcyc  43578  fsuppind  43598  aomclem8  44047  hbtlem5  44114  unielss  44204  ifpbi1  44462  ifpbi12  44473  ifpbi13  44474  ntrneik2  45077  ntrneikb  45079  gneispacess2  45131  2sbc6g  45384  sbiota1  45403  relpeq2  45913  nregmodel  45985  uzwo4  46039  iineq12dv  46090  fsumiunss  46556  limsupre  46620  limsupref  46664  limsupbnd1f  46665  limsupmnf  46700  limsupre2  46704  limsupmnfuzlem  46705  limsupre2mpt  46709  limsupre3  46712  limsupre3mpt  46713  ioodvbdlimc1lem2  46911  ioodvbdlimc2lem  46913  dvmptfprodlem  46923  wallispilem3  47046  fourierdlem48  47133  sge0f1o  47361  sge0iunmptlemre  47394  sge0iunmpt  47397  vonioo  47661  vonicc  47664  fcoresf1  48108  2reu8i  48152  2reuimp0  48153  2reuimp  48154  sprsymrelfolem2  48544  paireqne  48562  nfermltlrev  48811  bgoldbachlt  48880  tgoldbachlt  48883  gpgedgiov  49132  gpgedg2ov  49133  gpgedg2iv  49134  pgnbgreunbgrlem1  49180  pgnbgreunbgrlem3  49185  pgnbgreunbgrlem4  49186  pgnbgreunbgrlem6  49191  pgnbgreunbgr  49192  smprngprmrng  49405  ply1mulgsumlem1  49467  ply1mulgsumlem2  49468  elbigo2  49633  elbigo2r  49634  imbi12d2  49870  postcposALT  50645  postc  50646  setrecseq  50757  aacllem  50908