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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  imbi12d  347  imbi1  350  imim21b  400  pm5.33  849  con3ALT  1101  norasslem3  1566  sbjust  2100  sbequ  2122  sb6  2124  19.21t  2246  sb4b  2507  drsb1  2527  cbvralsvw  3317  sbralie  3342  raleqf  3345  ralcom2  3366  rmoeq1  3400  rspceaimv  3586  ralxpxfr2d  3603  alexeqg  3608  elab6g  3626  mo2icl  3675  sbc19.21g  3813  csbiebg  3883  ralss  3986  r19.37zv  4466  reuprg0  4664  unissb  4906  intmin4  4942  dftr2c  5221  ssexgOLD  5292  pocl  5574  vtoclr  5721  frsn  5747  cotrg  6123  dffun2  6576  fun11  6644  funimass4  6980  dff13  7289  f1mpt  7296  isopolem  7384  fnssintima  7403  oprabidw  7482  oprabid  7483  caovcan  7657  imaeqalov  7692  caoftrn  7766  ordunisuc2  7889  tfisi  7904  tfinds  7905  tfindsg  7906  tfindsg2  7907  dfom2  7913  findsg  7943  frxp  8175  xpord2indlem  8201  xpord3inddlem  8208  poseq  8212  frrlem12  8353  dfsmo2  8393  qliftfun  8861  ecoptocl  8866  ecopovtrn  8879  dom2lem  9057  findcard  9217  findcard2  9218  ssfi  9226  findcard3  9312  fiint  9356  supmo  9481  eqsup  9485  suplub  9489  supisoex  9504  infmo  9526  wemaplem1  9577  wemaplem2  9578  wemapsolem  9581  oemapvali  9722  cantnf  9731  wemapwe  9735  ttrclss  9758  kardenOLD  9997  setrec1lem1  10003  aceq1  10235  zorn2lem1  10613  axrepndlem2  10717  axregndlem2  10727  gruurn  10922  indpi  11031  nqereu  11053  prcdnq  11117  supexpr  11178  ltsosr  11218  supsrlem  11235  supsr  11236  axpre-lttrn  11290  axpre-sup  11293  prodgt0  12204  infm3  12316  prime  12820  raluz  13063  zsupss  13104  uzsupss  13107  xrsupsslem  13477  xrinfmsslem  13478  fz1sbc  13774  ssnn0fi  14168  fi1uzind  14693  brfi1indALT  14696  wrdind  14913  wrd2ind  14914  relexprelg  15234  rtrclreclem3  15256  relexpindlem  15259  relexpind  15260  rtrclind  15261  sgn3da  15297  sgnnbi  15300  sgnpbi  15301  rexanre  15558  rexico  15565  reusq0  15676  limsupgle  15688  ello12  15727  ello12r  15728  ello1d  15734  elo12  15738  elo12r  15739  lo1resb  15775  o1resb  15777  rlimcn3  15801  addcn2  15805  mulcn2  15807  lo1le  15863  rpnnen2lem12  16437  sqrt2irr  16461  dfgcd2  16763  exprmfct  16924  isprm5  16927  isprm7  16928  prmdvdsexpr  16937  prmpwdvds  17126  vdwmc2  17201  ramtlecl  17222  ramub  17235  rami  17237  ramcl  17251  firest  17653  mreexexd  17872  acsfn  17883  prslem  18521  ispos  18538  posi  18541  isposd  18546  pospropd  18549  lubeldm  18575  lubval  18578  glbeldm  18588  glbval  18591  joinval2lem  18602  meetval2lem  18616  resspos  18653  odlem1  19800  mndodcongi  19808  gexlem1  19844  sylow1lem3  19865  efgredlemb  20011  efgred  20013  frgpnabllem1  20138  isrrg  21001  isdomn4  21018  domnlcanb  21022  domnrcanb  21024  acsfn1p  21107  prmidlval  21669  xrsdsreclb  21772  islindf4  22199  mplsubglem  22361  mpllsslem  22362  ltbval  22407  opsrval  22410  psdmul  22542  mdetunilem1  22982  mdetunilem3  22984  mdetunilem4  22985  mdetunilem9  22990  chpscmat  23215  istopg  23268  isclo2  23461  neiptoptop  23504  neiptopnei  23505  lmbr  23631  ist0  23693  ist1-2  23720  t1sep2  23742  cmpfi  23781  2ndcdisj  23830  1stccn  23837  iskgen3  23923  ptpjopn  23986  hausdiag  24019  xkopt  24029  ist0-4  24103  isr0  24111  r0sep  24122  fbfinnfr  24215  fmfnfmlem2  24329  fmfnfmlem4  24331  fmfnfm  24332  cnflf  24376  cnfcf  24416  tmdgsum2  24470  tsmsf1o  24519  tsmsxplem1  24527  ustssel  24580  ustincl  24582  ustdiag  24583  ustinvel  24584  ustexhalf  24585  ust0  24594  ustuqtop4  24618  utopsnneiplem  24621  isucn2  24652  iducn  24656  metcnp  24915  txmetcnp  24921  metucn  24945  ngptgp  25010  nlmvscnlem1  25060  xrge0tsms  25209  xmetdcn2  25212  addcnlem  25239  ipcnlem1  25621  caucfil  25659  metcld  25682  metcld2  25683  ellimc2  26252  dvne0  26386  mdegleb  26437  mdegle0  26450  ply1divex  26510  fta1g  26543  dgrco  26649  plydivex  26673  fta1  26684  vieta1  26690  cxpcn3lem  27132  rlimcnp  27350  mpodvdsmulf1o  27578  dvdsmulf1o  27580  ppiublem1  27586  dchrinv  27645  lgseisenlem2  27760  2sqlem6  27807  2sqlem8  27810  2sqlem10  27812  nocvxminlem  28197  addsprop  28419  leadds1  28432  negsprop  28478  mulsprop  28573  bdayons  28719  onsfi  28799  expsne0  28879  istrkgc  28973  istrkgb  28974  axtgcgrid  28982  axtg5seg  28984  axtgpasch  28986  axtgeucl  28991  tgcgr4  29051  axlowdimlem15  29591  usgr2wlkneq  30399  usgr2pthlem  30406  isacycgr1  30809  acycgrcycl  30810  friendshipgt3  31056  isnvlem  31269  vacn  31353  smcnlem  31356  norm3lemt  31811  isch2  31882  chlimi  31893  omlsii  32062  eigorth  32497  stcltr1i  32933  elat2  32999  funcnv5mpt  33359  xrge0infss  33448  wrdt2ind  33612  xrge0tsmsd  33733  elrgspnlem4  33905  islinds5  34027  islbs5  34039  rprmdvdspow  34169  1arithufdlem3  34182  evl1deg1  34211  evl1deg2  34212  evl1deg3  34213  ply1dg1rt  34215  ist0cld  34576  qqhucn  34735  esum2d  34836  eulerpartlemgvv  35119  tgoldbachgt  35403  axtgupdim2ALTV  35408  bnj1145  35734  bnj1171  35741  bnj1172  35742  tz9.1regs  35943  srepdf  36128  erdszelem8  36171  satfrnmapom  36343  mclsval  36536  mclsax  36542  mclsppslem  36556  climuzcnv  36644  mirimanofffr  36670  elintfv  36745  ifscgr  37024  idinside  37064  brsegle  37088  ixpeq12dv  37220  trer  37319  filnetlem4  37384  axtcond  37481  axuntco  37482  dfttc4lem1  37531  mh-setindnd  37540  mh-unprimbi  37547  mh-regprimbi  37548  mh-infprim2bi  37550  bj-ssblem1  37768  bj-ssblem2  37769  bj-ax12  37771  bj-19.21t0  37957  mobidvALT  37984  currysetlem  38073  currysetlem1  38075  wl-ax12v2cl  38697  wl-sbrimt  38747  fin2so  38798  ptrecube  38806  poimirlem26  38832  poimirlem27  38833  heicant  38841  mbfresfi  38852  itg2addnc  38860  findcard4  38900  filbcmb  38940  sdclem2  38942  fdc  38945  fdc1  38946  rngoidmlem  39136  divrngidl  39228  pridlval  39233  smprngopr  39252  inecmo  39553  elcnvrefrels3  39813  eldisjdmqsim2  40014  qmapeldisjsim  40058  rnqmapeleldisjsim  40060  disjlem18  40101  ax12inda  40271  ax12v2-o  40272  isat3  40630  iscvlat2N  40647  psubspset  41067  ldilfset  41431  ldilset  41432  dilfsetN  41475  dilsetN  41476  cdlemefrs29bpre0  41719  cdlemefrs29clN  41722  cdlemefrs32fva  41723  cdlemn11pre  42533  dihord2pre  42548  lpolsetN  42805  isprimroot  43409  primrootsunit1  43413  primrootscoprbij  43418  aks6d1c1  43432  hashscontpow  43438  sticksstones11  43472  sticksstones12a  43473  aks6d1c6lem3  43488  fimgmcyc  43864  fsuppind  43884  aomclem8  44329  hbtlem5  44395  unielss  44481  ifpbi1  44739  ifpbi12  44750  ifpbi13  44751  ntrneik2  45353  ntrneikb  45355  gneispacess2  45407  2sbc6g  45660  sbiota1  45678  relpeq2  46199  nregmodel  46271  uzwo4  46344  iineq12dv  46394  fsumiunss  46860  limsupre  46924  limsupref  46968  limsupbnd1f  46969  limsupmnf  47004  limsupre2  47008  limsupmnfuzlem  47009  limsupre2mpt  47013  limsupre3  47016  limsupre3mpt  47017  ioodvbdlimc1lem2  47215  ioodvbdlimc2lem  47217  dvmptfprodlem  47227  wallispilem3  47350  fourierdlem48  47437  sge0f1o  47665  sge0iunmptlemre  47698  sge0iunmpt  47701  vonioo  47965  vonicc  47968  fcoresf1  48412  2reu8i  48457  2reuimp0  48458  2reuimp  48459  sprsymrelfolem2  48848  paireqne  48866  nfermltlrev  49115  bgoldbachlt  49184  tgoldbachlt  49187  gpgedgiov  49436  gpgedg2ov  49437  gpgedg2iv  49438  pgnbgreunbgrlem1  49484  pgnbgreunbgrlem3  49489  pgnbgreunbgrlem4  49490  pgnbgreunbgrlem6  49495  pgnbgreunbgr  49496  smprngprmrng  49767  ply1mulgsumlem1  49829  ply1mulgsumlem2  49830  elbigo2  49995  elbigo2r  49996  imbi12d2  50232  postcposALT  51037  postc  51038  setrecseq  51194  aacllem  51367