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  836  con3ALT  1084  norasslem3  1532  sbjust  2060  sbequ  2080  sb6  2082  19.21t  2203  sb4b  2477  drsb1  2497  cbvralsvw  3314  raleqf  3350  ralcom2  3374  rmoeq1  3413  rspceaimv  3627  ralxpxfr2d  3645  alexeqg  3650  elab6g  3668  mo2icl  3722  sbc19.21g  3868  csbiebg  3940  ralss  4069  r19.37zv  4507  reuprg0  4706  unissb  4943  intmin4  4981  dftr2c  5267  ssexg  5328  pocl  5604  vtoclr  5751  frsn  5775  cotrg  6129  dffun2  6572  fun11  6641  funimass4  6972  dff13  7274  f1mpt  7280  isopolem  7364  fnssintima  7381  oprabidw  7461  oprabid  7462  caovcan  7636  imaeqalov  7671  caoftrn  7736  ordunisuc2  7864  tfisi  7879  tfinds  7880  tfindsg  7881  tfindsg2  7882  dfom2  7888  findsg  7919  frxp  8149  xpord2indlem  8170  xpord3inddlem  8177  poseq  8181  frrlem12  8320  dfsmo2  8385  qliftfun  8840  ecoptocl  8845  ecopovtrn  8858  dom2lem  9030  findcard  9201  findcard2  9202  ssfi  9211  findcard3  9315  findcard3OLD  9316  fiint  9363  fiintOLD  9364  supmo  9489  eqsup  9493  suplub  9497  supisoex  9511  infmo  9532  wemaplem1  9583  wemaplem2  9584  wemapsolem  9587  oemapvali  9721  cantnf  9730  wemapwe  9734  ttrclss  9757  karden  9932  aceq1  10154  zorn2lem1  10533  axrepndlem2  10630  axregndlem2  10640  gruurn  10835  indpi  10944  nqereu  10966  prcdnq  11030  supexpr  11091  ltsosr  11131  supsrlem  11148  supsr  11149  axpre-lttrn  11203  axpre-sup  11206  prodgt0  12111  infm3  12224  prime  12696  raluz  12935  zsupss  12976  uzsupss  12979  xrsupsslem  13345  xrinfmsslem  13346  fz1sbc  13636  ssnn0fi  14022  fi1uzind  14542  brfi1indALT  14545  wrdind  14756  wrd2ind  14757  relexprelg  15073  rtrclreclem3  15095  relexpindlem  15098  relexpind  15099  rtrclind  15100  rexanre  15381  rexico  15388  reusq0  15497  limsupgle  15509  ello12  15548  ello12r  15549  ello1d  15555  elo12  15559  elo12r  15560  lo1resb  15596  o1resb  15598  rlimcn3  15622  addcn2  15626  mulcn2  15628  lo1le  15684  rpnnen2lem12  16257  sqrt2irr  16281  dfgcd2  16579  exprmfct  16737  isprm5  16740  isprm7  16741  prmdvdsexpr  16750  prmpwdvds  16937  vdwmc2  17012  ramtlecl  17033  ramub  17046  rami  17048  ramcl  17062  firest  17478  mreexexd  17692  acsfn  17703  prslem  18354  ispos  18371  posi  18374  isposd  18380  pospropd  18384  lubeldm  18410  lubval  18413  glbeldm  18423  glbval  18426  joinval2lem  18437  meetval2lem  18451  odlem1  19567  mndodcongi  19575  gexlem1  19611  sylow1lem3  19632  efgredlemb  19778  efgred  19780  frgpnabllem1  19905  isrrg  20714  isdomn4  20732  domnlcanb  20736  domnrcanb  20738  acsfn1p  20816  xrsdsreclb  21448  islindf4  21875  mplsubglem  22036  mpllsslem  22037  ltbval  22078  opsrval  22081  psdmul  22187  mdetunilem1  22633  mdetunilem3  22635  mdetunilem4  22636  mdetunilem9  22641  chpscmat  22863  istopg  22916  isclo2  23111  neiptoptop  23154  neiptopnei  23155  lmbr  23281  ist0  23343  ist1-2  23370  t1sep2  23392  cmpfi  23431  2ndcdisj  23479  1stccn  23486  iskgen3  23572  ptpjopn  23635  hausdiag  23668  xkopt  23678  ist0-4  23752  isr0  23760  r0sep  23771  fbfinnfr  23864  fmfnfmlem2  23978  fmfnfmlem4  23980  fmfnfm  23981  cnflf  24025  cnfcf  24065  tmdgsum2  24119  tsmsf1o  24168  tsmsxplem1  24176  ustssel  24229  ustincl  24231  ustdiag  24232  ustinvel  24233  ustexhalf  24234  ust0  24243  ustuqtop4  24268  utopsnneiplem  24271  isucn2  24303  iducn  24307  metcnp  24569  txmetcnp  24575  metucn  24599  ngptgp  24664  nlmvscnlem1  24722  xrge0tsms  24869  xmetdcn2  24872  addcnlem  24899  ipcnlem1  25292  caucfil  25330  metcld  25353  metcld2  25354  ellimc2  25926  dvne0  26064  mdegleb  26117  mdegle0  26130  ply1divex  26190  fta1g  26223  dgrco  26329  plydivex  26353  fta1  26364  vieta1  26368  cxpcn3lem  26804  rlimcnp  27022  mpodvdsmulf1o  27251  dvdsmulf1o  27253  ppiublem1  27260  dchrinv  27319  lgseisenlem2  27434  2sqlem6  27481  2sqlem8  27484  2sqlem10  27486  nocvxminlem  27836  addsprop  28023  sleadd1  28036  negsprop  28081  mulsprop  28170  expsne0  28428  istrkgc  28476  istrkgb  28477  axtgcgrid  28485  axtg5seg  28487  axtgpasch  28489  axtgeucl  28494  tgcgr4  28553  axlowdimlem15  28985  usgr2wlkneq  29788  usgr2pthlem  29795  friendshipgt3  30426  isnvlem  30638  vacn  30722  smcnlem  30725  norm3lemt  31180  isch2  31251  chlimi  31262  omlsii  31431  eigorth  31866  stcltr1i  32302  elat2  32368  funcnv5mpt  32684  xrge0infss  32770  wrdt2ind  32922  resspos  32940  xrge0tsmsd  33047  elrgspnlem4  33234  domnlcanOLD  33263  islinds5  33374  islbs5  33387  prmidlval  33444  rprmdvdspow  33540  1arithufdlem3  33553  evl1deg1  33580  evl1deg2  33581  evl1deg3  33582  ply1dg1rt  33583  ist0cld  33793  qqhucn  33954  esum2d  34073  eulerpartlemgvv  34357  sgn3da  34522  sgnnbi  34526  sgnpbi  34527  tgoldbachgt  34656  axtgupdim2ALTV  34661  bnj1145  34985  bnj1171  34992  bnj1172  34993  isacycgr1  35130  acycgrcycl  35131  erdszelem8  35182  satfrnmapom  35354  mclsval  35547  mclsax  35553  mclsppslem  35567  climuzcnv  35655  elintfv  35745  ifscgr  36025  idinside  36065  brsegle  36089  ixpeq12dv  36198  trer  36298  filnetlem4  36363  bj-ssblem1  36636  bj-ssblem2  36637  bj-ax12  36639  bj-19.21t0  36812  mobidvALT  36839  currysetlem  36927  currysetlem1  36929  wl-ax12v2cl  37486  wl-sbrimt  37527  fin2so  37593  ptrecube  37606  poimirlem26  37632  poimirlem27  37633  heicant  37641  mbfresfi  37652  itg2addnc  37660  filbcmb  37726  sdclem2  37728  fdc  37731  fdc1  37732  rngoidmlem  37922  divrngidl  38014  pridlval  38019  smprngopr  38038  inecmo  38336  elcnvrefrels3  38516  disjlem18  38781  ax12inda  38929  ax12v2-o  38930  isat3  39288  iscvlat2N  39305  psubspset  39726  ldilfset  40090  ldilset  40091  dilfsetN  40134  dilsetN  40135  cdlemefrs29bpre0  40378  cdlemefrs29clN  40381  cdlemefrs32fva  40382  cdlemn11pre  41192  dihord2pre  41207  lpolsetN  41464  isprimroot  42074  primrootsunit1  42078  primrootscoprbij  42083  aks6d1c1  42097  hashscontpow  42103  sticksstones11  42137  sticksstones12a  42138  aks6d1c6lem3  42153  fimgmcyc  42520  fsuppind  42576  aomclem8  43049  hbtlem5  43116  unielss  43206  ifpbi1  43466  ifpbi12  43477  ifpbi13  43478  ntrneik2  44081  ntrneikb  44083  gneispacess2  44135  2sbc6g  44410  sbiota1  44429  uzwo4  44992  iineq12dv  45045  fsumiunss  45530  limsupre  45596  limsupref  45640  limsupbnd1f  45641  limsupmnf  45676  limsupre2  45680  limsupmnfuzlem  45681  limsupre2mpt  45685  limsupre3  45688  limsupre3mpt  45689  ioodvbdlimc1lem2  45887  ioodvbdlimc2lem  45889  dvmptfprodlem  45899  wallispilem3  46022  fourierdlem48  46109  sge0f1o  46337  sge0iunmptlemre  46370  sge0iunmpt  46373  vonioo  46637  vonicc  46640  fcoresf1  47018  2reu8i  47062  2reuimp0  47063  2reuimp  47064  sprsymrelfolem2  47417  paireqne  47435  nfermltlrev  47668  bgoldbachlt  47737  tgoldbachlt  47740  ply1mulgsumlem1  48231  ply1mulgsumlem2  48232  elbigo2  48401  elbigo2r  48402  logic1  48639  postcposALT  48883  postc  48884  setrecseq  48915  setrec1lem1  48917  aacllem  49031