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  1085  norasslem3  1533  sbjust  2063  sbequ  2083  sb6  2085  19.21t  2207  sb4b  2483  drsb1  2503  cbvralsvw  3323  raleqf  3361  ralcom2  3385  rmoeq1  3425  rspceaimv  3641  ralxpxfr2d  3659  alexeqg  3664  elab6g  3682  mo2icl  3736  sbc19.21g  3882  csbiebg  3954  ralss  4083  r19.37zv  4525  reuprg0  4727  unissb  4963  intmin4  5001  dftr2c  5286  ssexg  5341  pocl  5615  poclOLD  5616  vtoclr  5763  frsn  5787  cotrg  6139  dffun2  6583  fun11  6652  funimass4  6986  dff13  7292  f1mpt  7298  isopolem  7381  fnssintima  7398  oprabidw  7479  oprabid  7480  caovcan  7654  imaeqalov  7689  caoftrn  7753  ordunisuc2  7881  tfisi  7896  tfinds  7897  tfindsg  7898  tfindsg2  7899  dfom2  7905  findsg  7937  frxp  8167  xpord2indlem  8188  xpord3inddlem  8195  poseq  8199  frrlem12  8338  dfsmo2  8403  qliftfun  8860  ecoptocl  8865  ecopovtrn  8878  dom2lem  9052  findcard  9229  findcard2  9230  ssfi  9240  findcard3  9346  findcard3OLD  9347  fiint  9394  fiintOLD  9395  supmo  9521  eqsup  9525  suplub  9529  supisoex  9543  infmo  9564  wemaplem1  9615  wemaplem2  9616  wemapsolem  9619  oemapvali  9753  cantnf  9762  wemapwe  9766  ttrclss  9789  karden  9964  aceq1  10186  zorn2lem1  10565  axrepndlem2  10662  axregndlem2  10672  gruurn  10867  indpi  10976  nqereu  10998  prcdnq  11062  supexpr  11123  ltsosr  11163  supsrlem  11180  supsr  11181  axpre-lttrn  11235  axpre-sup  11238  prodgt0  12141  infm3  12254  prime  12724  raluz  12961  zsupss  13002  uzsupss  13005  xrsupsslem  13369  xrinfmsslem  13370  fz1sbc  13660  ssnn0fi  14036  fi1uzind  14556  brfi1indALT  14559  wrdind  14770  wrd2ind  14771  relexprelg  15087  rtrclreclem3  15109  relexpindlem  15112  relexpind  15113  rtrclind  15114  rexanre  15395  rexico  15402  reusq0  15511  limsupgle  15523  ello12  15562  ello12r  15563  ello1d  15569  elo12  15573  elo12r  15574  lo1resb  15610  o1resb  15612  rlimcn3  15636  addcn2  15640  mulcn2  15642  lo1le  15700  rpnnen2lem12  16273  sqrt2irr  16297  dfgcd2  16593  exprmfct  16751  isprm5  16754  isprm7  16755  prmdvdsexpr  16764  prmpwdvds  16951  vdwmc2  17026  ramtlecl  17047  ramub  17060  rami  17062  ramcl  17076  firest  17492  mreexexd  17706  acsfn  17717  prslem  18368  ispos  18384  posi  18387  isposd  18393  pospropd  18397  lubeldm  18423  lubval  18426  glbeldm  18436  glbval  18439  joinval2lem  18450  meetval2lem  18464  odlem1  19577  mndodcongi  19585  gexlem1  19621  sylow1lem3  19642  efgredlemb  19788  efgred  19790  frgpnabllem1  19915  isrrg  20720  isdomn4  20738  domnlcanb  20742  domnrcanb  20744  acsfn1p  20822  xrsdsreclb  21454  islindf4  21881  mplsubglem  22042  mpllsslem  22043  ltbval  22084  opsrval  22087  psdmul  22193  mdetunilem1  22639  mdetunilem3  22641  mdetunilem4  22642  mdetunilem9  22647  chpscmat  22869  istopg  22922  isclo2  23117  neiptoptop  23160  neiptopnei  23161  lmbr  23287  ist0  23349  ist1-2  23376  t1sep2  23398  cmpfi  23437  2ndcdisj  23485  1stccn  23492  iskgen3  23578  ptpjopn  23641  hausdiag  23674  xkopt  23684  ist0-4  23758  isr0  23766  r0sep  23777  fbfinnfr  23870  fmfnfmlem2  23984  fmfnfmlem4  23986  fmfnfm  23987  cnflf  24031  cnfcf  24071  tmdgsum2  24125  tsmsf1o  24174  tsmsxplem1  24182  ustssel  24235  ustincl  24237  ustdiag  24238  ustinvel  24239  ustexhalf  24240  ust0  24249  ustuqtop4  24274  utopsnneiplem  24277  isucn2  24309  iducn  24313  metcnp  24575  txmetcnp  24581  metucn  24605  ngptgp  24670  nlmvscnlem1  24728  xrge0tsms  24875  xmetdcn2  24878  addcnlem  24905  ipcnlem1  25298  caucfil  25336  metcld  25359  metcld2  25360  ellimc2  25932  dvne0  26070  mdegleb  26123  mdegle0  26136  ply1divex  26196  fta1g  26229  dgrco  26335  plydivex  26357  fta1  26368  vieta1  26372  cxpcn3lem  26808  rlimcnp  27026  mpodvdsmulf1o  27255  dvdsmulf1o  27257  ppiublem1  27264  dchrinv  27323  lgseisenlem2  27438  2sqlem6  27485  2sqlem8  27488  2sqlem10  27490  nocvxminlem  27840  addsprop  28027  sleadd1  28040  negsprop  28085  mulsprop  28174  expsne0  28432  istrkgc  28480  istrkgb  28481  axtgcgrid  28489  axtg5seg  28491  axtgpasch  28493  axtgeucl  28498  tgcgr4  28557  axlowdimlem15  28989  usgr2wlkneq  29792  usgr2pthlem  29799  friendshipgt3  30430  isnvlem  30642  vacn  30726  smcnlem  30729  norm3lemt  31184  isch2  31255  chlimi  31266  omlsii  31435  eigorth  31870  stcltr1i  32306  elat2  32372  funcnv5mpt  32686  xrge0infss  32767  wrdt2ind  32920  resspos  32939  xrge0tsmsd  33041  domnlcanOLD  33249  islinds5  33360  islbs5  33373  prmidlval  33430  rprmdvdspow  33526  1arithufdlem3  33539  evl1deg1  33566  evl1deg2  33567  evl1deg3  33568  ply1dg1rt  33569  ist0cld  33779  qqhucn  33938  esum2d  34057  eulerpartlemgvv  34341  sgn3da  34506  sgnnbi  34510  sgnpbi  34511  tgoldbachgt  34640  axtgupdim2ALTV  34645  bnj1145  34969  bnj1171  34976  bnj1172  34977  isacycgr1  35114  acycgrcycl  35115  erdszelem8  35166  satfrnmapom  35338  mclsval  35531  mclsax  35537  mclsppslem  35551  climuzcnv  35639  elintfv  35728  ifscgr  36008  idinside  36048  brsegle  36072  ixpeq12dv  36182  trer  36282  filnetlem4  36347  bj-ssblem1  36620  bj-ssblem2  36621  bj-ax12  36623  bj-19.21t0  36796  mobidvALT  36823  currysetlem  36911  currysetlem1  36913  wl-sbrimt  37501  fin2so  37567  ptrecube  37580  poimirlem26  37606  poimirlem27  37607  heicant  37615  mbfresfi  37626  itg2addnc  37634  filbcmb  37700  sdclem2  37702  fdc  37705  fdc1  37706  rngoidmlem  37896  divrngidl  37988  pridlval  37993  smprngopr  38012  inecmo  38311  elcnvrefrels3  38491  disjlem18  38756  ax12inda  38904  ax12v2-o  38905  isat3  39263  iscvlat2N  39280  psubspset  39701  ldilfset  40065  ldilset  40066  dilfsetN  40109  dilsetN  40110  cdlemefrs29bpre0  40353  cdlemefrs29clN  40356  cdlemefrs32fva  40357  cdlemn11pre  41167  dihord2pre  41182  lpolsetN  41439  isprimroot  42050  primrootsunit1  42054  primrootscoprbij  42059  aks6d1c1  42073  hashscontpow  42079  sticksstones11  42113  sticksstones12a  42114  aks6d1c6lem3  42129  fimgmcyc  42489  fsuppind  42545  aomclem8  43018  hbtlem5  43085  unielss  43179  ifpbi1  43439  ifpbi12  43450  ifpbi13  43451  ntrneik2  44054  ntrneikb  44056  gneispacess2  44108  2sbc6g  44384  sbiota1  44403  uzwo4  44955  iineq12dv  45008  fsumiunss  45496  limsupre  45562  limsupref  45606  limsupbnd1f  45607  limsupmnf  45642  limsupre2  45646  limsupmnfuzlem  45647  limsupre2mpt  45651  limsupre3  45654  limsupre3mpt  45655  ioodvbdlimc1lem2  45853  ioodvbdlimc2lem  45855  dvmptfprodlem  45865  wallispilem3  45988  fourierdlem48  46075  sge0f1o  46303  sge0iunmptlemre  46336  sge0iunmpt  46339  vonioo  46603  vonicc  46606  fcoresf1  46984  2reu8i  47028  2reuimp0  47029  2reuimp  47030  sprsymrelfolem2  47367  paireqne  47385  nfermltlrev  47618  bgoldbachlt  47687  tgoldbachlt  47690  ply1mulgsumlem1  48115  ply1mulgsumlem2  48116  elbigo2  48286  elbigo2r  48287  logic1  48524  postcposALT  48748  postc  48749  setrecseq  48777  setrec1lem1  48779  aacllem  48895