Theorem imbi1d 343

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

Syntax hints:   → wi 4   ↔ wb 208

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 209

This theorem is referenced by:  imbi12d  346  imbi1  349  imim21b  398  pm5.33  846  con3ALT  1095  norasslem3  1555  rename-sb  2088  sbequ  2115  sb6  2117  19.21t  2240  sb4b  2505  drsb1  2525  cbvralsvw  3312  sbralie  3339  raleqf  3342  ralcom2  3363  rmoeq1  3397  rspceaimv  3586  ralxpxfr2d  3604  alexeqg  3609  elab6g  3627  mo2icl  3675  sbc19.21g  3813  csbiebg  3882  ralss  4007  ralssOLD  4009  r19.37zv  4458  reuprg0  4658  unissb  4896  intmin4  4932  dftr2c  5207  ssexg  5276  pocl  5559  vtoclr  5706  frsn  5731  cotrg  6094  dffun2  6526  fun11  6590  funimass4  6926  dff13  7233  f1mpt  7240  isopolem  7324  fnssintima  7341  oprabidw  7422  oprabid  7423  caovcan  7595  imaeqalov  7630  caoftrn  7696  ordunisuc2  7819  tfisi  7834  tfinds  7835  tfindsg  7836  tfindsg2  7837  dfom2  7843  findsg  7873  frxp  8100  xpord2indlem  8121  xpord3inddlem  8128  poseq  8132  frrlem12  8272  dfsmo2  8312  qliftfun  8778  ecoptocl  8783  ecopovtrn  8796  dom2lem  8967  findcard  9126  findcard2  9127  ssfi  9135  findcard3  9221  fiint  9265  supmo  9392  eqsup  9396  suplub  9400  supisoex  9415  infmo  9437  wemaplem1  9488  wemaplem2  9489  wemapsolem  9492  oemapvali  9633  cantnf  9642  wemapwe  9646  ttrclss  9669  karden  9847  aceq1  10067  zorn2lem1  10447  axrepndlem2  10545  axregndlem2  10555  gruurn  10750  indpi  10859  nqereu  10881  prcdnq  10945  supexpr  11006  ltsosr  11046  supsrlem  11063  supsr  11064  axpre-lttrn  11118  axpre-sup  11121  prodgt0  12032  infm3  12145  prime  12648  raluz  12891  zsupss  12932  uzsupss  12935  xrsupsslem  13304  xrinfmsslem  13305  fz1sbc  13599  ssnn0fi  13992  fi1uzind  14514  brfi1indALT  14517  wrdind  14729  wrd2ind  14730  relexprelg  15045  rtrclreclem3  15067  relexpindlem  15070  relexpind  15071  rtrclind  15072  sgn3da  15105  sgnnbi  15108  sgnpbi  15109  rexanre  15365  rexico  15372  reusq0  15483  limsupgle  15495  ello12  15534  ello12r  15535  ello1d  15541  elo12  15545  elo12r  15546  lo1resb  15582  o1resb  15584  rlimcn3  15608  addcn2  15612  mulcn2  15614  lo1le  15670  rpnnen2lem12  16248  sqrt2irr  16272  dfgcd2  16571  exprmfct  16730  isprm5  16733  isprm7  16734  prmdvdsexpr  16743  prmpwdvds  16931  vdwmc2  17006  ramtlecl  17027  ramub  17040  rami  17042  ramcl  17056  firest  17452  mreexexd  17671  acsfn  17682  prslem  18320  ispos  18337  posi  18340  isposd  18345  pospropd  18348  lubeldm  18374  lubval  18377  glbeldm  18387  glbval  18390  joinval2lem  18401  meetval2lem  18415  resspos  18452  odlem1  19566  mndodcongi  19574  gexlem1  19610  sylow1lem3  19631  efgredlemb  19777  efgred  19779  frgpnabllem1  19904  isrrg  20735  isdomn4  20753  domnlcanb  20757  domnrcanb  20759  acsfn1p  20836  xrsdsreclb  21454  islindf4  21878  mplsubglem  22038  mpllsslem  22039  ltbval  22084  opsrval  22087  psdmul  22219  mdetunilem1  22660  mdetunilem3  22662  mdetunilem4  22663  mdetunilem9  22668  chpscmat  22890  istopg  22943  isclo2  23136  neiptoptop  23179  neiptopnei  23180  lmbr  23306  ist0  23368  ist1-2  23395  t1sep2  23417  cmpfi  23456  2ndcdisj  23504  1stccn  23511  iskgen3  23597  ptpjopn  23660  hausdiag  23693  xkopt  23703  ist0-4  23777  isr0  23785  r0sep  23796  fbfinnfr  23889  fmfnfmlem2  24003  fmfnfmlem4  24005  fmfnfm  24006  cnflf  24050  cnfcf  24090  tmdgsum2  24144  tsmsf1o  24193  tsmsxplem1  24201  ustssel  24254  ustincl  24256  ustdiag  24257  ustinvel  24258  ustexhalf  24259  ust0  24268  ustuqtop4  24292  utopsnneiplem  24295  isucn2  24326  iducn  24330  metcnp  24589  txmetcnp  24595  metucn  24619  ngptgp  24684  nlmvscnlem1  24734  xrge0tsms  24883  xmetdcn2  24886  addcnlem  24913  ipcnlem1  25295  caucfil  25333  metcld  25356  metcld2  25357  ellimc2  25927  dvne0  26061  mdegleb  26112  mdegle0  26125  ply1divex  26185  fta1g  26218  dgrco  26323  plydivex  26349  fta1  26360  vieta1  26364  cxpcn3lem  26800  rlimcnp  27018  mpodvdsmulf1o  27246  dvdsmulf1o  27248  ppiublem1  27254  dchrinv  27313  lgseisenlem2  27428  2sqlem6  27475  2sqlem8  27478  2sqlem10  27480  nocvxminlem  27835  addsprop  28057  leadds1  28070  negsprop  28116  mulsprop  28211  bdayons  28357  onsfi  28437  expsne0  28517  istrkgc  28611  istrkgb  28612  axtgcgrid  28620  axtg5seg  28622  axtgpasch  28624  axtgeucl  28629  tgcgr4  28688  axlowdimlem15  29114  usgr2wlkneq  29913  usgr2pthlem  29920  friendshipgt3  30557  isnvlem  30770  vacn  30854  smcnlem  30857  norm3lemt  31312  isch2  31383  chlimi  31394  omlsii  31563  eigorth  31998  stcltr1i  32434  elat2  32500  funcnv5mpt  32830  xrge0infss  32923  wrdt2ind  33092  xrge0tsmsd  33214  elrgspnlem4  33387  domnlcanOLD  33425  islinds5  33514  islbs5  33527  prmidlval  33584  rprmdvdspow  33690  1arithufdlem3  33703  evl1deg1  33733  evl1deg2  33734  evl1deg3  33735  ply1dg1rt  33737  ist0cld  34091  qqhucn  34250  esum2d  34351  eulerpartlemgvv  34634  tgoldbachgt  34918  axtgupdim2ALTV  34923  bnj1145  35249  bnj1171  35256  bnj1172  35257  tz9.1regs  35391  isacycgr1  35457  acycgrcycl  35458  erdszelem8  35509  satfrnmapom  35681  mclsval  35874  mclsax  35880  mclsppslem  35894  climuzcnv  35982  elintfv  36076  ifscgr  36355  idinside  36395  brsegle  36419  ixpeq12dv  36537  trer  36637  filnetlem4  36702  axtcond  36799  axuntco  36800  dfttc4lem1  36849  mh-setindnd  36858  mh-unprimbi  36865  mh-regprimbi  36866  mh-infprim2bi  36868  bj-ssblem1  37087  bj-ssblem2  37088  bj-ax12  37090  bj-19.21t0  37276  mobidvALT  37303  currysetlem  37391  currysetlem1  37393  wl-ax12v2cl  37961  wl-sbrimt  38011  fin2so  38067  ptrecube  38080  poimirlem26  38106  poimirlem27  38107  heicant  38115  mbfresfi  38126  itg2addnc  38134  filbcmb  38200  sdclem2  38202  fdc  38205  fdc1  38206  rngoidmlem  38396  divrngidl  38488  pridlval  38493  smprngopr  38512  inecmo  38815  elcnvrefrels3  39075  eldisjdmqsim2  39276  qmapeldisjsim  39320  rnqmapeleldisjsim  39322  disjlem18  39363  ax12inda  39533  ax12v2-o  39534  isat3  39892  iscvlat2N  39909  psubspset  40329  ldilfset  40693  ldilset  40694  dilfsetN  40737  dilsetN  40738  cdlemefrs29bpre0  40981  cdlemefrs29clN  40984  cdlemefrs32fva  40985  cdlemn11pre  41795  dihord2pre  41810  lpolsetN  42067  isprimroot  42671  primrootsunit1  42675  primrootscoprbij  42680  aks6d1c1  42694  hashscontpow  42700  sticksstones11  42734  sticksstones12a  42735  aks6d1c6lem3  42750  fimgmcyc  43113  fsuppind  43133  aomclem8  43599  hbtlem5  43666  unielss  43756  ifpbi1  44014  ifpbi12  44025  ifpbi13  44026  ntrneik2  44629  ntrneikb  44631  gneispacess2  44683  2sbc6g  44952  sbiota1  44971  relpeq2  45482  nregmodel  45554  uzwo4  45594  iineq12dv  45645  fsumiunss  46112  limsupre  46176  limsupref  46220  limsupbnd1f  46221  limsupmnf  46256  limsupre2  46260  limsupmnfuzlem  46261  limsupre2mpt  46265  limsupre3  46268  limsupre3mpt  46269  ioodvbdlimc1lem2  46467  ioodvbdlimc2lem  46469  dvmptfprodlem  46479  wallispilem3  46602  fourierdlem48  46689  sge0f1o  46917  sge0iunmptlemre  46950  sge0iunmpt  46953  vonioo  47217  vonicc  47220  fcoresf1  47624  2reu8i  47668  2reuimp0  47669  2reuimp  47670  sprsymrelfolem2  48060  paireqne  48078  nfermltlrev  48327  bgoldbachlt  48396  tgoldbachlt  48399  gpgedgiov  48648  gpgedg2ov  48649  gpgedg2iv  48650  pgnbgreunbgrlem1  48696  pgnbgreunbgrlem3  48701  pgnbgreunbgrlem4  48702  pgnbgreunbgrlem6  48707  pgnbgreunbgr  48708  ply1mulgsumlem1  48969  ply1mulgsumlem2  48970  elbigo2  49135  elbigo2r  49136  logic1  49373  postcposALT  50150  postc  50151  setrecseq  50267  setrec1lem1  50269  aacllem  50383