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  1537  sbjust  2066  sbequ  2086  sb6  2088  19.21t  2209  sb4b  2475  drsb1  2495  cbvralsvw  3283  sbralie  3318  raleqf  3321  ralcom2  3343  rmoeq1  3377  rspceaimv  3578  ralxpxfr2d  3596  alexeqg  3601  elab6g  3619  mo2icl  3668  sbc19.21g  3808  csbiebg  3877  ralss  4004  ralssOLD  4006  r19.37zv  4447  reuprg0  4650  unissb  4886  intmin4  4922  dftr2c  5196  ssexg  5256  pocl  5527  vtoclr  5674  frsn  5699  cotrg  6053  dffun2  6486  fun11  6550  funimass4  6881  dff13  7183  f1mpt  7190  isopolem  7274  fnssintima  7291  oprabidw  7372  oprabid  7373  caovcan  7545  imaeqalov  7580  caoftrn  7646  ordunisuc2  7769  tfisi  7784  tfinds  7785  tfindsg  7786  tfindsg2  7787  dfom2  7793  findsg  7822  frxp  8051  xpord2indlem  8072  xpord3inddlem  8079  poseq  8083  frrlem12  8222  dfsmo2  8262  qliftfun  8721  ecoptocl  8726  ecopovtrn  8739  dom2lem  8909  findcard  9068  findcard2  9069  ssfi  9077  findcard3  9162  fiint  9206  supmo  9331  eqsup  9335  suplub  9339  supisoex  9354  infmo  9376  wemaplem1  9427  wemaplem2  9428  wemapsolem  9431  oemapvali  9569  cantnf  9578  wemapwe  9582  ttrclss  9605  karden  9783  aceq1  10003  zorn2lem1  10382  axrepndlem2  10479  axregndlem2  10489  gruurn  10684  indpi  10793  nqereu  10815  prcdnq  10879  supexpr  10940  ltsosr  10980  supsrlem  10997  supsr  10998  axpre-lttrn  11052  axpre-sup  11055  prodgt0  11963  infm3  12076  prime  12549  raluz  12789  zsupss  12830  uzsupss  12833  xrsupsslem  13201  xrinfmsslem  13202  fz1sbc  13495  ssnn0fi  13887  fi1uzind  14409  brfi1indALT  14412  wrdind  14624  wrd2ind  14625  relexprelg  14940  rtrclreclem3  14962  relexpindlem  14965  relexpind  14966  rtrclind  14967  rexanre  15249  rexico  15256  reusq0  15367  limsupgle  15379  ello12  15418  ello12r  15419  ello1d  15425  elo12  15429  elo12r  15430  lo1resb  15466  o1resb  15468  rlimcn3  15492  addcn2  15496  mulcn2  15498  lo1le  15554  rpnnen2lem12  16129  sqrt2irr  16153  dfgcd2  16452  exprmfct  16610  isprm5  16613  isprm7  16614  prmdvdsexpr  16623  prmpwdvds  16811  vdwmc2  16886  ramtlecl  16907  ramub  16920  rami  16922  ramcl  16936  firest  17331  mreexexd  17549  acsfn  17560  prslem  18198  ispos  18215  posi  18218  isposd  18223  pospropd  18226  lubeldm  18252  lubval  18255  glbeldm  18265  glbval  18268  joinval2lem  18279  meetval2lem  18293  resspos  18330  odlem1  19442  mndodcongi  19450  gexlem1  19486  sylow1lem3  19507  efgredlemb  19653  efgred  19655  frgpnabllem1  19780  isrrg  20608  isdomn4  20626  domnlcanb  20630  domnrcanb  20632  acsfn1p  20709  xrsdsreclb  21345  islindf4  21770  mplsubglem  21931  mpllsslem  21932  ltbval  21973  opsrval  21976  psdmul  22076  mdetunilem1  22522  mdetunilem3  22524  mdetunilem4  22525  mdetunilem9  22530  chpscmat  22752  istopg  22805  isclo2  22998  neiptoptop  23041  neiptopnei  23042  lmbr  23168  ist0  23230  ist1-2  23257  t1sep2  23279  cmpfi  23318  2ndcdisj  23366  1stccn  23373  iskgen3  23459  ptpjopn  23522  hausdiag  23555  xkopt  23565  ist0-4  23639  isr0  23647  r0sep  23658  fbfinnfr  23751  fmfnfmlem2  23865  fmfnfmlem4  23867  fmfnfm  23868  cnflf  23912  cnfcf  23952  tmdgsum2  24006  tsmsf1o  24055  tsmsxplem1  24063  ustssel  24116  ustincl  24118  ustdiag  24119  ustinvel  24120  ustexhalf  24121  ust0  24130  ustuqtop4  24154  utopsnneiplem  24157  isucn2  24188  iducn  24192  metcnp  24451  txmetcnp  24457  metucn  24481  ngptgp  24546  nlmvscnlem1  24596  xrge0tsms  24745  xmetdcn2  24748  addcnlem  24775  ipcnlem1  25167  caucfil  25205  metcld  25228  metcld2  25229  ellimc2  25800  dvne0  25938  mdegleb  25991  mdegle0  26004  ply1divex  26064  fta1g  26097  dgrco  26203  plydivex  26227  fta1  26238  vieta1  26242  cxpcn3lem  26679  rlimcnp  26897  mpodvdsmulf1o  27126  dvdsmulf1o  27128  ppiublem1  27135  dchrinv  27194  lgseisenlem2  27309  2sqlem6  27356  2sqlem8  27359  2sqlem10  27361  nocvxminlem  27712  addsprop  27914  sleadd1  27927  negsprop  27972  mulsprop  28064  bdayon  28204  onsfi  28278  expsne0  28354  istrkgc  28427  istrkgb  28428  axtgcgrid  28436  axtg5seg  28438  axtgpasch  28440  axtgeucl  28445  tgcgr4  28504  axlowdimlem15  28929  usgr2wlkneq  29729  usgr2pthlem  29736  friendshipgt3  30370  isnvlem  30582  vacn  30666  smcnlem  30669  norm3lemt  31124  isch2  31195  chlimi  31206  omlsii  31375  eigorth  31810  stcltr1i  32246  elat2  32312  funcnv5mpt  32642  xrge0infss  32735  sgn3da  32809  sgnnbi  32813  sgnpbi  32814  wrdt2ind  32926  xrge0tsmsd  33034  elrgspnlem4  33204  domnlcanOLD  33238  islinds5  33324  islbs5  33337  prmidlval  33394  rprmdvdspow  33490  1arithufdlem3  33503  evl1deg1  33531  evl1deg2  33532  evl1deg3  33533  ply1dg1rt  33535  ist0cld  33838  qqhucn  33997  esum2d  34098  eulerpartlemgvv  34381  tgoldbachgt  34668  axtgupdim2ALTV  34673  bnj1145  34997  bnj1171  35004  bnj1172  35005  tz9.1regs  35122  isacycgr1  35182  acycgrcycl  35183  erdszelem8  35234  satfrnmapom  35406  mclsval  35599  mclsax  35605  mclsppslem  35619  climuzcnv  35707  elintfv  35801  ifscgr  36078  idinside  36118  brsegle  36142  ixpeq12dv  36250  trer  36350  filnetlem4  36415  bj-ssblem1  36688  bj-ssblem2  36689  bj-ax12  36691  bj-19.21t0  36864  mobidvALT  36891  currysetlem  36979  currysetlem1  36981  wl-ax12v2cl  37540  wl-sbrimt  37581  fin2so  37647  ptrecube  37660  poimirlem26  37686  poimirlem27  37687  heicant  37695  mbfresfi  37706  itg2addnc  37714  filbcmb  37780  sdclem2  37782  fdc  37785  fdc1  37786  rngoidmlem  37976  divrngidl  38068  pridlval  38073  smprngopr  38092  inecmo  38383  elcnvrefrels3  38572  disjlem18  38838  ax12inda  38987  ax12v2-o  38988  isat3  39346  iscvlat2N  39363  psubspset  39783  ldilfset  40147  ldilset  40148  dilfsetN  40191  dilsetN  40192  cdlemefrs29bpre0  40435  cdlemefrs29clN  40438  cdlemefrs32fva  40439  cdlemn11pre  41249  dihord2pre  41264  lpolsetN  41521  isprimroot  42126  primrootsunit1  42130  primrootscoprbij  42135  aks6d1c1  42149  hashscontpow  42155  sticksstones11  42189  sticksstones12a  42190  aks6d1c6lem3  42205  fimgmcyc  42567  fsuppind  42623  aomclem8  43094  hbtlem5  43161  unielss  43251  ifpbi1  43510  ifpbi12  43521  ifpbi13  43522  ntrneik2  44125  ntrneikb  44127  gneispacess2  44179  2sbc6g  44448  sbiota1  44467  relpeq2  44978  nregmodel  45050  uzwo4  45090  iineq12dv  45143  fsumiunss  45615  limsupre  45679  limsupref  45723  limsupbnd1f  45724  limsupmnf  45759  limsupre2  45763  limsupmnfuzlem  45764  limsupre2mpt  45768  limsupre3  45771  limsupre3mpt  45772  ioodvbdlimc1lem2  45970  ioodvbdlimc2lem  45972  dvmptfprodlem  45982  wallispilem3  46105  fourierdlem48  46192  sge0f1o  46420  sge0iunmptlemre  46453  sge0iunmpt  46456  vonioo  46720  vonicc  46723  fcoresf1  47100  2reu8i  47144  2reuimp0  47145  2reuimp  47146  sprsymrelfolem2  47524  paireqne  47542  nfermltlrev  47775  bgoldbachlt  47844  tgoldbachlt  47847  gpgedgiov  48096  gpgedg2ov  48097  gpgedg2iv  48098  pgnbgreunbgrlem1  48144  pgnbgreunbgrlem3  48149  pgnbgreunbgrlem4  48150  pgnbgreunbgrlem6  48155  pgnbgreunbgr  48156  ply1mulgsumlem1  48418  ply1mulgsumlem2  48419  elbigo2  48584  elbigo2r  48585  logic1  48822  postcposALT  49600  postc  49601  setrecseq  49717  setrec1lem1  49719  aacllem  49833