Theorem imbi1d 345

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

Syntax hints:   → wi 4   ↔ wb 209

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 210

This theorem is referenced by:  imbi12d  348  imbi1  351  imim21b  398  pm5.33  836  con3ALT  1087  norasslem3  1538  sbjust  2071  sbequ  2091  sb6  2093  19.21t  2206  sb4b  2474  sb4bOLD  2475  drsb1  2498  ralcom2  3265  raleqf  3299  rspceaimv  3532  ralxpxfr2d  3543  alexeqg  3548  elab6g  3568  mo2icl  3616  sbc19.21g  3760  csbiebg  3831  ralss  3957  r19.37zv  4399  reuprg0  4604  intmin4  4874  ssexg  5201  pocl  5460  poclOLD  5461  vtoclr  5597  frsn  5621  fun11  6432  funimass4  6755  dff13  7045  f1mpt  7051  isopolem  7132  oprabidw  7222  oprabid  7223  caovcan  7390  caoftrn  7484  ordunisuc2  7601  tfisi  7615  tfinds  7616  tfindsg  7617  tfindsg2  7618  dfom2  7624  findsg  7655  frxp  7871  frrlem12  8016  dfsmo2  8062  qliftfun  8462  ecoptocl  8467  ecopovtrn  8480  dom2lem  8646  findcard  8819  findcard2  8820  ssfi  8829  findcard2OLD  8891  findcard3  8892  fiint  8926  supmo  9046  eqsup  9050  suplub  9054  supisoex  9068  infmo  9089  wemaplem1  9140  wemaplem2  9141  wemapsolem  9144  oemapvali  9277  cantnf  9286  wemapwe  9290  karden  9476  aceq1  9696  zorn2lem1  10075  axrepndlem2  10172  axregndlem2  10182  pwfseqlem4  10241  gruurn  10377  indpi  10486  nqereu  10508  prcdnq  10572  supexpr  10633  ltsosr  10673  supsrlem  10690  supsr  10691  axpre-lttrn  10745  axpre-sup  10748  prodgt0  11644  infm3  11756  prime  12223  raluz  12457  zsupss  12498  uzsupss  12501  xrsupsslem  12862  xrinfmsslem  12863  fz1sbc  13153  ssnn0fi  13523  fi1uzind  14028  brfi1indALT  14031  wrdind  14252  wrd2ind  14253  relexprelg  14566  rtrclreclem3  14588  relexpindlem  14591  relexpind  14592  rtrclind  14593  rexanre  14875  rexico  14882  reusq0  14991  limsupgle  15003  ello12  15042  ello12r  15043  ello1d  15049  elo12  15053  elo12r  15054  lo1resb  15090  o1resb  15092  rlimcn3  15116  addcn2  15120  mulcn2  15122  lo1le  15180  rpnnen2lem12  15749  sqrt2irr  15773  dfgcd2  16069  exprmfct  16224  isprm5  16227  isprm7  16228  prmdvdsexpr  16237  prmpwdvds  16420  vdwmc2  16495  ramtlecl  16516  ramub  16529  rami  16531  ramcl  16545  firest  16891  mreexexd  17105  acsfn  17116  prslem  17759  ispos  17775  posi  17778  isposd  17784  pospropd  17787  lubeldm  17813  lubval  17816  glbeldm  17826  glbval  17829  joinval2lem  17840  meetval2lem  17854  odlem1  18881  mndodcongi  18889  gexlem1  18922  sylow1lem3  18943  efgredlemb  19090  efgred  19092  frgpnabllem1  19212  acsfn1p  19797  isrrg  20280  xrsdsreclb  20364  islindf4  20754  mplsubglem  20915  mpllsslem  20916  ltbval  20954  opsrval  20957  mdetunilem1  21463  mdetunilem3  21465  mdetunilem4  21466  mdetunilem9  21471  chpscmat  21693  istopg  21746  isclo2  21939  neiptoptop  21982  neiptopnei  21983  lmbr  22109  ist0  22171  ist1-2  22198  t1sep2  22220  cmpfi  22259  2ndcdisj  22307  1stccn  22314  iskgen3  22400  ptpjopn  22463  hausdiag  22496  xkopt  22506  ist0-4  22580  isr0  22588  r0sep  22599  fbfinnfr  22692  fmfnfmlem2  22806  fmfnfmlem4  22808  fmfnfm  22809  cnflf  22853  cnfcf  22893  tmdgsum2  22947  tsmsf1o  22996  tsmsxplem1  23004  ustssel  23057  ustincl  23059  ustdiag  23060  ustinvel  23061  ustexhalf  23062  ust0  23071  ustuqtop4  23096  utopsnneiplem  23099  isucn2  23130  iducn  23134  metcnp  23393  txmetcnp  23399  metucn  23423  ngptgp  23488  nlmvscnlem1  23538  xrge0tsms  23685  xmetdcn2  23688  addcnlem  23715  ipcnlem1  24096  caucfil  24134  metcld  24157  metcld2  24158  ellimc2  24728  dvne0  24862  mdegleb  24916  mdegle0  24929  ply1divex  24988  fta1g  25019  dgrco  25123  plydivex  25144  fta1  25155  vieta1  25159  cxpcn3lem  25587  rlimcnp  25802  dvdsmulf1o  26030  ppiublem1  26037  dchrinv  26096  lgseisenlem2  26211  2sqlem6  26258  2sqlem8  26261  2sqlem10  26263  istrkgc  26499  istrkgb  26500  axtgcgrid  26508  axtg5seg  26510  axtgpasch  26512  axtgeucl  26517  tgcgr4  26576  axlowdimlem15  27001  usgr2wlkneq  27797  usgr2pthlem  27804  friendshipgt3  28435  isnvlem  28645  vacn  28729  smcnlem  28732  norm3lemt  29187  isch2  29258  chlimi  29269  omlsii  29438  eigorth  29873  stcltr1i  30309  elat2  30375  funcnv5mpt  30679  xrge0infss  30757  wrdt2ind  30899  resspos  30917  xrge0tsmsd  30990  islinds5  31231  prmidlval  31280  ist0cld  31451  qqhucn  31608  esum2d  31727  eulerpartlemgvv  32009  sgn3da  32174  sgnnbi  32178  sgnpbi  32179  tgoldbachgt  32309  axtgupdim2ALTV  32314  bnj1145  32640  bnj1171  32647  bnj1172  32648  isacycgr1  32775  acycgrcycl  32776  erdszelem8  32827  satfrnmapom  32999  mclsval  33192  mclsax  33198  mclsppslem  33212  climuzcnv  33296  fnssintima  33345  elintfv  33408  xpord2ind  33474  xpord3ind  33480  poseq  33482  nocvxminlem  33658  ifscgr  34032  idinside  34072  brsegle  34096  trer  34191  filnetlem4  34256  bj-ssblem1  34521  bj-ssblem2  34522  bj-ax12  34524  bj-19.21t0  34699  mobidvALT  34727  currysetlem  34820  currysetlem1  34822  wl-sbrimt  35391  fin2so  35450  ptrecube  35463  poimirlem26  35489  poimirlem27  35490  heicant  35498  mbfresfi  35509  itg2addnc  35517  filbcmb  35584  sdclem2  35586  fdc  35589  fdc1  35590  rngoidmlem  35780  divrngidl  35872  pridlval  35877  smprngopr  35896  inecmo  36173  elcnvrefrels3  36335  ax12inda  36648  ax12v2-o  36649  isat3  37007  iscvlat2N  37024  psubspset  37444  ldilfset  37808  ldilset  37809  dilfsetN  37852  dilsetN  37853  cdlemefrs29bpre0  38096  cdlemefrs29clN  38099  cdlemefrs32fva  38100  cdlemn11pre  38910  dihord2pre  38925  lpolsetN  39182  sticksstones11  39781  sticksstones12a  39782  isdomn4  39835  fsuppind  39930  aomclem8  40530  hbtlem5  40597  ifpbi1  40710  ifpbi12  40721  ifpbi13  40722  ntrneik2  41320  ntrneikb  41322  gneispacess2  41374  2sbc6g  41647  sbiota1  41666  uzwo4  42215  fsumiunss  42734  limsupre  42800  limsupref  42844  limsupbnd1f  42845  limsupmnf  42880  limsupre2  42884  limsupmnfuzlem  42885  limsupre2mpt  42889  limsupre3  42892  limsupre3mpt  42893  ioodvbdlimc1lem2  43091  ioodvbdlimc2lem  43093  dvmptfprodlem  43103  wallispilem3  43226  fourierdlem48  43313  sge0f1o  43538  sge0iunmptlemre  43571  sge0iunmpt  43574  vonioo  43838  vonicc  43841  fcoresf1  44178  2reu8i  44220  2reuimp0  44221  2reuimp  44222  sprsymrelfolem2  44561  paireqne  44579  nfermltlrev  44812  bgoldbachlt  44881  tgoldbachlt  44884  ply1mulgsumlem1  45343  ply1mulgsumlem2  45344  elbigo2  45514  elbigo2r  45515  logic1  45752  postcposALT  45976  postc  45977  setrecseq  46005  setrec1lem1  46007  aacllem  46119