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  3290  sbralie  3326  raleqf  3329  ralcom2  3351  rmoeq1  3387  rspceaimv  3594  ralxpxfr2d  3612  alexeqg  3617  elab6g  3635  mo2icl  3685  sbc19.21g  3825  csbiebg  3894  ralss  4021  ralssOLD  4023  r19.37zv  4465  reuprg0  4666  unissb  4903  intmin4  4941  dftr2c  5217  ssexg  5278  pocl  5554  vtoclr  5701  frsn  5726  cotrg  6080  dffun2  6521  fun11  6590  funimass4  6925  dff13  7229  f1mpt  7236  isopolem  7320  fnssintima  7337  oprabidw  7418  oprabid  7419  caovcan  7593  imaeqalov  7628  caoftrn  7694  ordunisuc2  7820  tfisi  7835  tfinds  7836  tfindsg  7837  tfindsg2  7838  dfom2  7844  findsg  7873  frxp  8105  xpord2indlem  8126  xpord3inddlem  8133  poseq  8137  frrlem12  8276  dfsmo2  8316  qliftfun  8775  ecoptocl  8780  ecopovtrn  8793  dom2lem  8963  findcard  9127  findcard2  9128  ssfi  9137  findcard3  9229  findcard3OLD  9230  fiint  9277  fiintOLD  9278  supmo  9403  eqsup  9407  suplub  9411  supisoex  9426  infmo  9448  wemaplem1  9499  wemaplem2  9500  wemapsolem  9503  oemapvali  9637  cantnf  9646  wemapwe  9650  ttrclss  9673  karden  9848  aceq1  10070  zorn2lem1  10449  axrepndlem2  10546  axregndlem2  10556  gruurn  10751  indpi  10860  nqereu  10882  prcdnq  10946  supexpr  11007  ltsosr  11047  supsrlem  11064  supsr  11065  axpre-lttrn  11119  axpre-sup  11122  prodgt0  12029  infm3  12142  prime  12615  raluz  12855  zsupss  12896  uzsupss  12899  xrsupsslem  13267  xrinfmsslem  13268  fz1sbc  13561  ssnn0fi  13950  fi1uzind  14472  brfi1indALT  14475  wrdind  14687  wrd2ind  14688  relexprelg  15004  rtrclreclem3  15026  relexpindlem  15029  relexpind  15030  rtrclind  15031  rexanre  15313  rexico  15320  reusq0  15431  limsupgle  15443  ello12  15482  ello12r  15483  ello1d  15489  elo12  15493  elo12r  15494  lo1resb  15530  o1resb  15532  rlimcn3  15556  addcn2  15560  mulcn2  15562  lo1le  15618  rpnnen2lem12  16193  sqrt2irr  16217  dfgcd2  16516  exprmfct  16674  isprm5  16677  isprm7  16678  prmdvdsexpr  16687  prmpwdvds  16875  vdwmc2  16950  ramtlecl  16971  ramub  16984  rami  16986  ramcl  17000  firest  17395  mreexexd  17609  acsfn  17620  prslem  18258  ispos  18275  posi  18278  isposd  18283  pospropd  18286  lubeldm  18312  lubval  18315  glbeldm  18325  glbval  18328  joinval2lem  18339  meetval2lem  18353  odlem1  19465  mndodcongi  19473  gexlem1  19509  sylow1lem3  19530  efgredlemb  19676  efgred  19678  frgpnabllem1  19803  isrrg  20607  isdomn4  20625  domnlcanb  20629  domnrcanb  20631  acsfn1p  20708  xrsdsreclb  21330  islindf4  21747  mplsubglem  21908  mpllsslem  21909  ltbval  21950  opsrval  21953  psdmul  22053  mdetunilem1  22499  mdetunilem3  22501  mdetunilem4  22502  mdetunilem9  22507  chpscmat  22729  istopg  22782  isclo2  22975  neiptoptop  23018  neiptopnei  23019  lmbr  23145  ist0  23207  ist1-2  23234  t1sep2  23256  cmpfi  23295  2ndcdisj  23343  1stccn  23350  iskgen3  23436  ptpjopn  23499  hausdiag  23532  xkopt  23542  ist0-4  23616  isr0  23624  r0sep  23635  fbfinnfr  23728  fmfnfmlem2  23842  fmfnfmlem4  23844  fmfnfm  23845  cnflf  23889  cnfcf  23929  tmdgsum2  23983  tsmsf1o  24032  tsmsxplem1  24040  ustssel  24093  ustincl  24095  ustdiag  24096  ustinvel  24097  ustexhalf  24098  ust0  24107  ustuqtop4  24132  utopsnneiplem  24135  isucn2  24166  iducn  24170  metcnp  24429  txmetcnp  24435  metucn  24459  ngptgp  24524  nlmvscnlem1  24574  xrge0tsms  24723  xmetdcn2  24726  addcnlem  24753  ipcnlem1  25145  caucfil  25183  metcld  25206  metcld2  25207  ellimc2  25778  dvne0  25916  mdegleb  25969  mdegle0  25982  ply1divex  26042  fta1g  26075  dgrco  26181  plydivex  26205  fta1  26216  vieta1  26220  cxpcn3lem  26657  rlimcnp  26875  mpodvdsmulf1o  27104  dvdsmulf1o  27106  ppiublem1  27113  dchrinv  27172  lgseisenlem2  27287  2sqlem6  27334  2sqlem8  27337  2sqlem10  27339  nocvxminlem  27689  addsprop  27883  sleadd1  27896  negsprop  27941  mulsprop  28033  bdayon  28173  onsfi  28247  expsne0  28321  istrkgc  28381  istrkgb  28382  axtgcgrid  28390  axtg5seg  28392  axtgpasch  28394  axtgeucl  28399  tgcgr4  28458  axlowdimlem15  28883  usgr2wlkneq  29686  usgr2pthlem  29693  friendshipgt3  30327  isnvlem  30539  vacn  30623  smcnlem  30626  norm3lemt  31081  isch2  31152  chlimi  31163  omlsii  31332  eigorth  31767  stcltr1i  32203  elat2  32269  funcnv5mpt  32592  xrge0infss  32683  sgn3da  32759  sgnnbi  32763  sgnpbi  32764  wrdt2ind  32875  resspos  32892  xrge0tsmsd  33002  elrgspnlem4  33196  domnlcanOLD  33230  islinds5  33338  islbs5  33351  prmidlval  33408  rprmdvdspow  33504  1arithufdlem3  33517  evl1deg1  33545  evl1deg2  33546  evl1deg3  33547  ply1dg1rt  33548  ist0cld  33823  qqhucn  33982  esum2d  34083  eulerpartlemgvv  34367  tgoldbachgt  34654  axtgupdim2ALTV  34659  bnj1145  34983  bnj1171  34990  bnj1172  34991  isacycgr1  35133  acycgrcycl  35134  erdszelem8  35185  satfrnmapom  35357  mclsval  35550  mclsax  35556  mclsppslem  35570  climuzcnv  35658  elintfv  35752  ifscgr  36032  idinside  36072  brsegle  36096  ixpeq12dv  36204  trer  36304  filnetlem4  36369  bj-ssblem1  36642  bj-ssblem2  36643  bj-ax12  36645  bj-19.21t0  36818  mobidvALT  36845  currysetlem  36933  currysetlem1  36935  wl-ax12v2cl  37494  wl-sbrimt  37535  fin2so  37601  ptrecube  37614  poimirlem26  37640  poimirlem27  37641  heicant  37649  mbfresfi  37660  itg2addnc  37668  filbcmb  37734  sdclem2  37736  fdc  37739  fdc1  37740  rngoidmlem  37930  divrngidl  38022  pridlval  38027  smprngopr  38046  inecmo  38337  elcnvrefrels3  38526  disjlem18  38792  ax12inda  38941  ax12v2-o  38942  isat3  39300  iscvlat2N  39317  psubspset  39738  ldilfset  40102  ldilset  40103  dilfsetN  40146  dilsetN  40147  cdlemefrs29bpre0  40390  cdlemefrs29clN  40393  cdlemefrs32fva  40394  cdlemn11pre  41204  dihord2pre  41219  lpolsetN  41476  isprimroot  42081  primrootsunit1  42085  primrootscoprbij  42090  aks6d1c1  42104  hashscontpow  42110  sticksstones11  42144  sticksstones12a  42145  aks6d1c6lem3  42160  fimgmcyc  42522  fsuppind  42578  aomclem8  43050  hbtlem5  43117  unielss  43207  ifpbi1  43466  ifpbi12  43477  ifpbi13  43478  ntrneik2  44081  ntrneikb  44083  gneispacess2  44135  2sbc6g  44404  sbiota1  44423  relpeq2  44935  nregmodel  45007  uzwo4  45047  iineq12dv  45100  fsumiunss  45573  limsupre  45639  limsupref  45683  limsupbnd1f  45684  limsupmnf  45719  limsupre2  45723  limsupmnfuzlem  45724  limsupre2mpt  45728  limsupre3  45731  limsupre3mpt  45732  ioodvbdlimc1lem2  45930  ioodvbdlimc2lem  45932  dvmptfprodlem  45942  wallispilem3  46065  fourierdlem48  46152  sge0f1o  46380  sge0iunmptlemre  46413  sge0iunmpt  46416  vonioo  46680  vonicc  46683  fcoresf1  47070  2reu8i  47114  2reuimp0  47115  2reuimp  47116  sprsymrelfolem2  47494  paireqne  47512  nfermltlrev  47745  bgoldbachlt  47814  tgoldbachlt  47817  gpgedgiov  48056  gpgedg2ov  48057  gpgedg2iv  48058  pgnbgreunbgrlem1  48103  pgnbgreunbgrlem3  48108  pgnbgreunbgrlem4  48109  pgnbgreunbgrlem6  48114  pgnbgreunbgr  48115  ply1mulgsumlem1  48375  ply1mulgsumlem2  48376  elbigo2  48541  elbigo2r  48542  logic1  48779  postcposALT  49557  postc  49558  setrecseq  49674  setrec1lem1  49676  aacllem  49790