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 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  347  imbi1  350  imim21b  397  pm5.33  833  con3ALT  1080  con3ALTOLD  1081  norasslem3  1532  sbjust  2068  sbequ  2090  sb6  2093  19.21t  2206  sb4b  2499  sb4bOLD  2500  drsb1  2535  ralcom2  3365  raleqf  3399  rspceaimv  3630  ralxpxfr2d  3641  alexeqg  3646  mo2icl  3707  sbc19.21g  3848  csbiebg  3917  ralss  4039  r19.37zv  4449  reuprg0  4640  intmin4  4907  ssexg  5229  pocl  5483  vtoclr  5617  frsn  5641  fun11  6430  funimass4  6732  dff13  7015  f1mpt  7021  isopolem  7100  oprabidw  7189  oprabid  7190  caovcan  7354  caoftrn  7446  ordunisuc2  7561  tfisi  7575  tfinds  7576  tfindsg  7577  tfindsg2  7578  dfom2  7584  findsg  7611  frxp  7822  dfsmo2  7986  qliftfun  8384  ecoptocl  8389  ecopovtrn  8402  dom2lem  8551  findcard  8759  findcard2  8760  findcard3  8763  fiint  8797  supmo  8918  eqsup  8922  suplub  8926  supisoex  8940  infmo  8961  wemaplem1  9012  wemaplem2  9013  wemapsolem  9016  oemapvali  9149  cantnf  9158  wemapwe  9162  karden  9326  aceq1  9545  zorn2lem1  9920  axrepndlem2  10017  axregndlem2  10027  pwfseqlem4  10086  gruurn  10222  indpi  10331  nqereu  10353  prcdnq  10417  supexpr  10478  ltsosr  10518  supsrlem  10535  supsr  10536  axpre-lttrn  10590  axpre-sup  10593  prodgt0  11489  infm3  11602  prime  12066  raluz  12299  zsupss  12340  uzsupss  12343  xrsupsslem  12703  xrinfmsslem  12704  fz1sbc  12986  ssnn0fi  13356  fi1uzind  13858  brfi1indALT  13861  wrdind  14086  wrd2ind  14087  relexprelg  14399  rtrclreclem3  14421  relexpindlem  14424  relexpind  14425  rtrclind  14426  rexanre  14708  rexico  14715  reusq0  14824  limsupgle  14836  ello12  14875  ello12r  14876  ello1d  14882  elo12  14886  elo12r  14887  lo1resb  14923  o1resb  14925  rlimcn2  14949  addcn2  14952  mulcn2  14954  lo1le  15010  rpnnen2lem12  15580  sqrt2irr  15604  dfgcd2  15896  exprmfct  16050  isprm5  16053  isprm7  16054  prmdvdsexpr  16063  prmpwdvds  16242  vdwmc2  16317  ramtlecl  16338  ramub  16351  rami  16353  ramcl  16367  firest  16708  mreexexd  16921  acsfn  16932  prslem  17543  ispos  17559  posi  17562  isposd  17567  lubeldm  17593  lubval  17596  glbeldm  17606  glbval  17609  joinval2lem  17620  meetval2lem  17634  pospropd  17746  odlem1  18665  mndodcongi  18673  gexlem1  18706  sylow1lem3  18727  efgredlemb  18874  efgred  18876  frgpnabllem1  18995  acsfn1p  19580  isrrg  20063  mplsubglem  20216  mpllsslem  20217  ltbval  20254  opsrval  20257  xrsdsreclb  20594  islindf4  20984  mdetunilem1  21223  mdetunilem3  21225  mdetunilem4  21226  mdetunilem9  21231  chpscmat  21452  istopg  21505  isclo2  21698  neiptoptop  21741  neiptopnei  21742  lmbr  21868  ist0  21930  ist1-2  21957  t1sep2  21979  cmpfi  22018  2ndcdisj  22066  1stccn  22073  iskgen3  22159  ptpjopn  22222  hausdiag  22255  xkopt  22265  ist0-4  22339  isr0  22347  r0sep  22358  fbfinnfr  22451  fmfnfmlem2  22565  fmfnfmlem4  22567  fmfnfm  22568  cnflf  22612  cnfcf  22652  tmdgsum2  22706  tsmsf1o  22755  tsmsxplem1  22763  ustssel  22816  ustincl  22818  ustdiag  22819  ustinvel  22820  ustexhalf  22821  ust0  22830  ustuqtop4  22855  utopsnneiplem  22858  isucn2  22890  iducn  22894  metcnp  23153  txmetcnp  23159  metucn  23183  ngptgp  23247  nlmvscnlem1  23297  xrge0tsms  23444  xmetdcn2  23447  addcnlem  23474  ipcnlem1  23850  caucfil  23888  metcld  23911  metcld2  23912  ellimc2  24477  dvne0  24610  mdegleb  24660  mdegle0  24673  ply1divex  24732  fta1g  24763  dgrco  24867  plydivex  24888  fta1  24899  vieta1  24903  cxpcn3lem  25330  rlimcnp  25545  dvdsmulf1o  25773  ppiublem1  25780  dchrinv  25839  lgseisenlem2  25954  2sqlem6  26001  2sqlem8  26004  2sqlem10  26006  istrkgc  26242  istrkgb  26243  axtgcgrid  26251  axtg5seg  26253  axtgpasch  26255  axtgeucl  26260  tgcgr4  26319  axlowdimlem15  26744  usgr2wlkneq  27539  usgr2pthlem  27546  friendshipgt3  28179  isnvlem  28389  vacn  28473  smcnlem  28476  norm3lemt  28931  isch2  29002  chlimi  29013  omlsii  29182  eigorth  29617  stcltr1i  30053  elat2  30119  funcnv5mpt  30415  xrge0infss  30486  wrdt2ind  30629  resspos  30648  xrge0tsmsd  30694  islinds5  30934  prmidlval  30956  qqhucn  31235  esum2d  31354  eulerpartlemgvv  31636  sgn3da  31801  sgnnbi  31805  sgnpbi  31806  tgoldbachgt  31936  axtgupdim2ALTV  31941  bnj1145  32267  bnj1171  32274  bnj1172  32275  isacycgr1  32395  acycgrcycl  32396  erdszelem8  32447  satfrnmapom  32619  mclsval  32812  mclsax  32818  mclsppslem  32832  climuzcnv  32916  elintfv  33009  poseq  33097  frrlem12  33136  nocvxminlem  33249  ifscgr  33507  idinside  33547  brsegle  33571  trer  33666  filnetlem4  33731  bj-ssblem1  33989  bj-ssblem2  33990  bj-ax12  33992  bj-19.21t0  34155  mobidvALT  34183  currysetlem  34258  currysetlem1  34260  wl-sbrimt  34788  wl-dfralflem  34840  fin2so  34881  ptrecube  34894  poimirlem26  34920  poimirlem27  34921  heicant  34929  mbfresfi  34940  itg2addnc  34948  filbcmb  35017  sdclem2  35019  fdc  35022  fdc1  35023  rngoidmlem  35216  divrngidl  35308  pridlval  35313  smprngopr  35332  inecmo  35611  elcnvrefrels3  35773  ax12inda  36086  ax12v2-o  36087  isat3  36445  iscvlat2N  36462  psubspset  36882  ldilfset  37246  ldilset  37247  dilfsetN  37290  dilsetN  37291  cdlemefrs29bpre0  37534  cdlemefrs29clN  37537  cdlemefrs32fva  37538  cdlemn11pre  38348  dihord2pre  38363  lpolsetN  38620  aomclem8  39668  hbtlem5  39735  ifpbi1  39850  ifpbi12  39861  ifpbi13  39862  ntrneik2  40449  ntrneikb  40451  gneispacess2  40503  2sbc6g  40754  sbiota1  40773  uzwo4  41322  fsumiunss  41863  limsupre  41929  limsupref  41973  limsupbnd1f  41974  limsupmnf  42009  limsupre2  42013  limsupmnfuzlem  42014  limsupre2mpt  42018  limsupre3  42021  limsupre3mpt  42022  ioodvbdlimc1lem2  42224  ioodvbdlimc2lem  42226  dvmptfprodlem  42236  wallispilem3  42359  fourierdlem48  42446  sge0f1o  42671  sge0iunmptlemre  42704  sge0iunmpt  42707  vonioo  42971  vonicc  42974  2reu8i  43319  2reuimp0  43320  2reuimp  43321  sprsymrelfolem2  43662  paireqne  43680  nfermltlrev  43916  bgoldbachlt  43985  tgoldbachlt  43988  ply1mulgsumlem1  44447  ply1mulgsumlem2  44448  elbigo2  44619  elbigo2r  44620  setrecseq  44795  setrec1lem1  44797  aacllem  44909