Theorem imbi1d 334

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

Syntax hints:   → wi 4   ↔ wb 198

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 199

This theorem is referenced by:  imbi12d  337  imbi1  340  imim21b  386  pm5.33  823  con3ALT  1065  con3ALTOLD  1066  sbjust  2014  sbequ  2035  sb6  2037  19.21t  2135  axc15OLD  2358  sb4b  2423  drsb1  2456  mobidOLD  2562  ralcom2  3304  raleqf  3337  rspceaimv  3543  ralxpxfr2d  3554  alexeqg  3559  mo2icl  3621  sbc19.21g  3751  csbiebg  3813  ralss  3929  r19.37zv  4331  reuprg0  4513  intmin4  4779  ssexg  5084  pocl  5334  vtoclr  5466  frsn  5490  fun11  6263  funimass4  6562  dff13  6840  f1mpt  6846  isopolem  6923  oprabid  7009  caovcan  7170  caoftrn  7264  ordunisuc2  7377  tfisi  7391  tfinds  7392  tfindsg  7393  tfindsg2  7394  dfom2  7400  findsg  7426  frxp  7627  dfsmo2  7790  qliftfun  8184  ecoptocl  8189  ecopovtrn  8202  dom2lem  8348  findcard  8554  findcard2  8555  findcard3  8558  fiint  8592  supmo  8713  eqsup  8717  suplub  8721  supisoex  8735  infmo  8756  wemaplem1  8807  wemaplem2  8808  wemapsolem  8811  oemapvali  8943  cantnf  8952  wemapwe  8956  karden  9120  aceq1  9339  zorn2lem1  9718  axrepndlem2  9815  axregndlem2  9825  pwfseqlem4  9884  gruurn  10020  indpi  10129  nqereu  10151  prcdnq  10215  supexpr  10276  ltsosr  10316  supsrlem  10333  supsr  10334  axpre-lttrn  10388  axpre-sup  10391  prodgt0  11290  infm3  11403  prime  11879  raluz  12113  zsupss  12154  uzsupss  12157  xrsupsslem  12519  xrinfmsslem  12520  fz1sbc  12802  ssnn0fi  13171  fi1uzind  13669  brfi1indALT  13672  wrdind  13918  wrdindOLD  13919  wrd2ind  13920  wrd2indOLD  13921  relexprelg  14261  rtrclreclem3  14283  relexpindlem  14286  relexpind  14287  rtrclind  14288  rexanre  14570  rexico  14577  reusq0  14686  limsupgle  14698  ello12  14737  ello12r  14738  ello1d  14744  elo12  14748  elo12r  14749  lo1resb  14785  o1resb  14787  rlimcn2  14811  addcn2  14814  mulcn2  14816  lo1le  14872  rpnnen2lem12  15441  sqrt2irr  15465  dfgcd2  15753  exprmfct  15907  isprm5  15910  isprm7  15911  prmdvdsexpr  15920  prmpwdvds  16099  vdwmc2  16174  ramtlecl  16195  ramub  16208  rami  16210  ramcl  16224  firest  16565  mreexexd  16780  acsfn  16791  prslem  17402  ispos  17418  posi  17421  isposd  17426  lubeldm  17452  lubval  17455  glbeldm  17465  glbval  17468  joinval2lem  17479  meetval2lem  17493  pospropd  17605  odlem1  18428  mndodcongi  18436  gexlem1  18468  sylow1lem3  18489  efgredlemb  18634  efgred  18637  frgpnabllem1  18752  acsfn1p  19303  isrrg  19785  mplsubglem  19931  mpllsslem  19932  ltbval  19968  opsrval  19971  xrsdsreclb  20297  islindf4  20687  mdetunilem1  20928  mdetunilem3  20930  mdetunilem4  20931  mdetunilem9  20936  chpscmat  21157  istopg  21210  isclo2  21403  neiptoptop  21446  neiptopnei  21447  lmbr  21573  ist0  21635  ist1-2  21662  t1sep2  21684  cmpfi  21723  2ndcdisj  21771  1stccn  21778  iskgen3  21864  ptpjopn  21927  hausdiag  21960  xkopt  21970  ist0-4  22044  isr0  22052  r0sep  22063  fbfinnfr  22156  fmfnfmlem2  22270  fmfnfmlem4  22272  fmfnfm  22273  cnflf  22317  cnfcf  22357  tmdgsum2  22411  tsmsf1o  22459  tsmsxplem1  22467  ustssel  22520  ustincl  22522  ustdiag  22523  ustinvel  22524  ustexhalf  22525  ust0  22534  ustuqtop4  22559  utopsnneiplem  22562  isucn2  22594  iducn  22598  metcnp  22857  txmetcnp  22863  metucn  22887  ngptgp  22951  nlmvscnlem1  23001  xrge0tsms  23148  xmetdcn2  23151  addcnlem  23178  ipcnlem1  23554  caucfil  23592  metcld  23615  metcld2  23616  ellimc2  24181  dvne0  24314  mdegleb  24364  mdegle0  24377  ply1divex  24436  fta1g  24467  dgrco  24571  plydivex  24592  fta1  24603  vieta1  24607  cxpcn3lem  25032  rlimcnp  25248  dvdsmulf1o  25476  ppiublem1  25483  dchrinv  25542  lgseisenlem2  25657  2sqlem6  25704  2sqlem8  25707  2sqlem10  25709  istrkgc  25945  istrkgb  25946  axtgcgrid  25954  axtg5seg  25956  axtgpasch  25958  axtgeucl  25963  tgcgr4  26022  axlowdimlem15  26448  usgr2wlkneq  27248  usgr2pthlem  27255  friendshipgt3  27958  isnvlem  28167  vacn  28251  smcnlem  28254  norm3lemt  28711  isch2  28782  chlimi  28793  omlsii  28964  eigorth  29399  stcltr1i  29835  elat2  29901  funcnv5mpt  30178  xrge0infss  30239  resspos  30378  cycpmcl  30450  xrge0tsmsd  30530  islinds5  30605  qqhucn  30877  esum2d  30996  eulerpartlemgvv  31279  sgn3da  31445  sgnnbi  31449  sgnpbi  31450  tgoldbachgt  31582  axtgupdim2OLD  31587  bnj1145  31910  bnj1171  31917  bnj1172  31918  erdszelem8  32030  mclsval  32330  mclsax  32336  mclsppslem  32350  climuzcnv  32434  elintfv  32527  poseq  32616  frrlem12  32655  nocvxminlem  32768  ifscgr  33026  idinside  33066  brsegle  33090  trer  33185  filnetlem4  33250  bj-ssblem1  33495  bj-ssblem2  33496  bj-ax12  33498  bj-19.21t  33644  mobidvALT  33672  currysetlem  33751  currysetlem1  33753  wl-sbrimt  34227  wl-dfralflem  34279  fin2so  34320  ptrecube  34333  poimirlem26  34359  poimirlem27  34360  heicant  34368  mbfresfi  34379  itg2addnc  34387  filbcmb  34457  sdclem2  34459  fdc  34462  fdc1  34463  rngoidmlem  34656  divrngidl  34748  pridlval  34753  smprngopr  34772  inecmo  35055  elcnvrefrels3  35216  ax12inda  35529  ax12v2-o  35530  isat3  35888  iscvlat2N  35905  psubspset  36325  ldilfset  36689  ldilset  36690  dilfsetN  36733  dilsetN  36734  cdlemefrs29bpre0  36977  cdlemefrs29clN  36980  cdlemefrs32fva  36981  cdlemn11pre  37791  dihord2pre  37806  lpolsetN  38063  aomclem8  39057  hbtlem5  39124  ifpbi1  39239  ifpbi12  39250  ifpbi13  39251  ntrneik2  39805  ntrneikb  39807  gneispacess2  39859  2sbc6g  40164  sbiota1  40183  uzwo4  40735  fsumiunss  41288  limsupre  41354  limsupref  41398  limsupbnd1f  41399  limsupmnf  41434  limsupre2  41438  limsupmnfuzlem  41439  limsupre2mpt  41443  limsupre3  41446  limsupre3mpt  41447  ioodvbdlimc1lem2  41648  ioodvbdlimc2lem  41650  dvmptfprodlem  41660  wallispilem3  41784  fourierdlem48  41871  sge0f1o  42096  sge0iunmptlemre  42129  sge0iunmpt  42132  vonioo  42396  vonicc  42399  2reu8i  42719  2reuimp0  42720  2reuimp  42721  sprsymrelfolem2  43024  paireqne  43042  nfermltlrev  43278  bgoldbachlt  43347  tgoldbachlt  43350  ply1mulgsumlem1  43808  ply1mulgsumlem2  43809  elbigo2  43981  elbigo2r  43982  setrecseq  44156  setrec1lem1  44158  aacllem  44270