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  2088  sb6  2090  19.21t  2211  sb4b  2477  drsb1  2497  cbvralsvw  3284  sbralie  3319  raleqf  3322  ralcom2  3344  rmoeq1  3378  rspceaimv  3579  ralxpxfr2d  3597  alexeqg  3602  elab6g  3620  mo2icl  3669  sbc19.21g  3809  csbiebg  3878  ralss  4005  ralssOLD  4007  r19.37zv  4457  reuprg0  4656  unissb  4893  intmin4  4929  dftr2c  5205  ssexg  5265  pocl  5537  vtoclr  5684  frsn  5709  cotrg  6065  dffun2  6499  fun11  6563  funimass4  6895  dff13  7197  f1mpt  7204  isopolem  7288  fnssintima  7305  oprabidw  7386  oprabid  7387  caovcan  7559  imaeqalov  7594  caoftrn  7660  ordunisuc2  7783  tfisi  7798  tfinds  7799  tfindsg  7800  tfindsg2  7801  dfom2  7807  findsg  7836  frxp  8065  xpord2indlem  8086  xpord3inddlem  8093  poseq  8097  frrlem12  8236  dfsmo2  8276  qliftfun  8735  ecoptocl  8740  ecopovtrn  8753  dom2lem  8925  findcard  9084  findcard2  9085  ssfi  9093  findcard3  9178  fiint  9222  supmo  9347  eqsup  9351  suplub  9355  supisoex  9370  infmo  9392  wemaplem1  9443  wemaplem2  9444  wemapsolem  9447  oemapvali  9585  cantnf  9594  wemapwe  9598  ttrclss  9621  karden  9799  aceq1  10019  zorn2lem1  10398  axrepndlem2  10495  axregndlem2  10505  gruurn  10700  indpi  10809  nqereu  10831  prcdnq  10895  supexpr  10956  ltsosr  10996  supsrlem  11013  supsr  11014  axpre-lttrn  11068  axpre-sup  11071  prodgt0  11979  infm3  12092  prime  12564  raluz  12800  zsupss  12841  uzsupss  12844  xrsupsslem  13213  xrinfmsslem  13214  fz1sbc  13507  ssnn0fi  13899  fi1uzind  14421  brfi1indALT  14424  wrdind  14636  wrd2ind  14637  relexprelg  14952  rtrclreclem3  14974  relexpindlem  14977  relexpind  14978  rtrclind  14979  rexanre  15261  rexico  15268  reusq0  15379  limsupgle  15391  ello12  15430  ello12r  15431  ello1d  15437  elo12  15441  elo12r  15442  lo1resb  15478  o1resb  15480  rlimcn3  15504  addcn2  15508  mulcn2  15510  lo1le  15566  rpnnen2lem12  16141  sqrt2irr  16165  dfgcd2  16464  exprmfct  16622  isprm5  16625  isprm7  16626  prmdvdsexpr  16635  prmpwdvds  16823  vdwmc2  16898  ramtlecl  16919  ramub  16932  rami  16934  ramcl  16948  firest  17343  mreexexd  17562  acsfn  17573  prslem  18211  ispos  18228  posi  18231  isposd  18236  pospropd  18239  lubeldm  18265  lubval  18268  glbeldm  18278  glbval  18281  joinval2lem  18292  meetval2lem  18306  resspos  18343  odlem1  19455  mndodcongi  19463  gexlem1  19499  sylow1lem3  19520  efgredlemb  19666  efgred  19668  frgpnabllem1  19793  isrrg  20622  isdomn4  20640  domnlcanb  20644  domnrcanb  20646  acsfn1p  20723  xrsdsreclb  21359  islindf4  21784  mplsubglem  21945  mpllsslem  21946  ltbval  21989  opsrval  21992  psdmul  22100  mdetunilem1  22547  mdetunilem3  22549  mdetunilem4  22550  mdetunilem9  22555  chpscmat  22777  istopg  22830  isclo2  23023  neiptoptop  23066  neiptopnei  23067  lmbr  23193  ist0  23255  ist1-2  23282  t1sep2  23304  cmpfi  23343  2ndcdisj  23391  1stccn  23398  iskgen3  23484  ptpjopn  23547  hausdiag  23580  xkopt  23590  ist0-4  23664  isr0  23672  r0sep  23683  fbfinnfr  23776  fmfnfmlem2  23890  fmfnfmlem4  23892  fmfnfm  23893  cnflf  23937  cnfcf  23977  tmdgsum2  24031  tsmsf1o  24080  tsmsxplem1  24088  ustssel  24141  ustincl  24143  ustdiag  24144  ustinvel  24145  ustexhalf  24146  ust0  24155  ustuqtop4  24179  utopsnneiplem  24182  isucn2  24213  iducn  24217  metcnp  24476  txmetcnp  24482  metucn  24506  ngptgp  24571  nlmvscnlem1  24621  xrge0tsms  24770  xmetdcn2  24773  addcnlem  24800  ipcnlem1  25192  caucfil  25230  metcld  25253  metcld2  25254  ellimc2  25825  dvne0  25963  mdegleb  26016  mdegle0  26029  ply1divex  26089  fta1g  26122  dgrco  26228  plydivex  26252  fta1  26263  vieta1  26267  cxpcn3lem  26704  rlimcnp  26922  mpodvdsmulf1o  27151  dvdsmulf1o  27153  ppiublem1  27160  dchrinv  27219  lgseisenlem2  27334  2sqlem6  27381  2sqlem8  27384  2sqlem10  27386  nocvxminlem  27737  addsprop  27939  sleadd1  27952  negsprop  27997  mulsprop  28089  bdayon  28229  onsfi  28303  expsne0  28379  istrkgc  28452  istrkgb  28453  axtgcgrid  28461  axtg5seg  28463  axtgpasch  28465  axtgeucl  28470  tgcgr4  28529  axlowdimlem15  28955  usgr2wlkneq  29755  usgr2pthlem  29762  friendshipgt3  30399  isnvlem  30611  vacn  30695  smcnlem  30698  norm3lemt  31153  isch2  31224  chlimi  31235  omlsii  31404  eigorth  31839  stcltr1i  32275  elat2  32341  funcnv5mpt  32672  xrge0infss  32768  sgn3da  32843  sgnnbi  32847  sgnpbi  32848  wrdt2ind  32963  xrge0tsmsd  33083  elrgspnlem4  33255  domnlcanOLD  33290  islinds5  33376  islbs5  33389  prmidlval  33446  rprmdvdspow  33542  1arithufdlem3  33555  evl1deg1  33585  evl1deg2  33586  evl1deg3  33587  ply1dg1rt  33589  ist0cld  33918  qqhucn  34077  esum2d  34178  eulerpartlemgvv  34461  tgoldbachgt  34748  axtgupdim2ALTV  34753  bnj1145  35077  bnj1171  35084  bnj1172  35085  tz9.1regs  35202  isacycgr1  35262  acycgrcycl  35263  erdszelem8  35314  satfrnmapom  35486  mclsval  35679  mclsax  35685  mclsppslem  35699  climuzcnv  35787  elintfv  35881  ifscgr  36160  idinside  36200  brsegle  36224  ixpeq12dv  36332  trer  36432  filnetlem4  36497  bj-ssblem1  36771  bj-ssblem2  36772  bj-ax12  36774  bj-19.21t0  36947  mobidvALT  36974  currysetlem  37062  currysetlem1  37064  wl-ax12v2cl  37623  wl-sbrimt  37664  fin2so  37720  ptrecube  37733  poimirlem26  37759  poimirlem27  37760  heicant  37768  mbfresfi  37779  itg2addnc  37787  filbcmb  37853  sdclem2  37855  fdc  37858  fdc1  37859  rngoidmlem  38049  divrngidl  38141  pridlval  38146  smprngopr  38165  inecmo  38460  elcnvrefrels3  38700  disjlem18  38971  ax12inda  39120  ax12v2-o  39121  isat3  39479  iscvlat2N  39496  psubspset  39916  ldilfset  40280  ldilset  40281  dilfsetN  40324  dilsetN  40325  cdlemefrs29bpre0  40568  cdlemefrs29clN  40571  cdlemefrs32fva  40572  cdlemn11pre  41382  dihord2pre  41397  lpolsetN  41654  isprimroot  42259  primrootsunit1  42263  primrootscoprbij  42268  aks6d1c1  42282  hashscontpow  42288  sticksstones11  42322  sticksstones12a  42323  aks6d1c6lem3  42338  fimgmcyc  42704  fsuppind  42748  aomclem8  43218  hbtlem5  43285  unielss  43375  ifpbi1  43634  ifpbi12  43645  ifpbi13  43646  ntrneik2  44249  ntrneikb  44251  gneispacess2  44303  2sbc6g  44572  sbiota1  44591  relpeq2  45102  nregmodel  45174  uzwo4  45214  iineq12dv  45266  fsumiunss  45737  limsupre  45801  limsupref  45845  limsupbnd1f  45846  limsupmnf  45881  limsupre2  45885  limsupmnfuzlem  45886  limsupre2mpt  45890  limsupre3  45893  limsupre3mpt  45894  ioodvbdlimc1lem2  46092  ioodvbdlimc2lem  46094  dvmptfprodlem  46104  wallispilem3  46227  fourierdlem48  46314  sge0f1o  46542  sge0iunmptlemre  46575  sge0iunmpt  46578  vonioo  46842  vonicc  46845  fcoresf1  47231  2reu8i  47275  2reuimp0  47276  2reuimp  47277  sprsymrelfolem2  47655  paireqne  47673  nfermltlrev  47906  bgoldbachlt  47975  tgoldbachlt  47978  gpgedgiov  48227  gpgedg2ov  48228  gpgedg2iv  48229  pgnbgreunbgrlem1  48275  pgnbgreunbgrlem3  48280  pgnbgreunbgrlem4  48281  pgnbgreunbgrlem6  48286  pgnbgreunbgr  48287  ply1mulgsumlem1  48548  ply1mulgsumlem2  48549  elbigo2  48714  elbigo2r  48715  logic1  48952  postcposALT  49729  postc  49730  setrecseq  49846  setrec1lem1  49848  aacllem  49962