Theorem imbi1d 332

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

Syntax hints:   → wi 4   ↔ wb 197

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 198

This theorem is referenced by:  imbi12d  335  imbi1  338  imim21b  383  pm5.33  855  con3ALT  1098  19.21t  2240  19.21tOLDOLD  2241  19.21tOLD  2387  axc15  2471  drsb1  2536  ralcom2  3292  raleqf  3323  rspceaimv  3510  ralxpxfr2d  3521  alexeqg  3526  mo2icl  3583  sbc19.21g  3698  csbiebg  3751  ralss  3865  r19.37zv  4262  intmin4  4698  ssexg  4999  pocl  5239  vtoclr  5364  frsn  5391  fun11  6170  funimass4  6464  dff13  6732  f1mpt  6738  isopolem  6815  oprabid  6901  caovcan  7064  caoftrn  7158  ordunisuc2  7270  tfisi  7284  tfinds  7285  tfindsg  7286  tfindsg2  7287  dfom2  7293  findsg  7319  frxp  7517  dfsmo2  7676  qliftfun  8063  ecoptocl  8068  ecopovtrn  8082  dom2lem  8228  findcard  8434  findcard2  8435  findcard3  8438  fiint  8472  supmo  8593  eqsup  8597  suplub  8601  supisoex  8615  infmo  8636  wemaplem1  8686  wemaplem2  8687  wemapsolem  8690  oemapvali  8824  cantnf  8833  wemapwe  8837  karden  9001  aceq1  9219  zorn2lem1  9599  axrepndlem2  9696  axregndlem2  9706  pwfseqlem4  9765  gruurn  9901  indpi  10010  nqereu  10032  prcdnq  10096  supexpr  10157  ltsosr  10196  supsrlem  10213  supsr  10214  axpre-lttrn  10268  axpre-sup  10271  prodgt0  11149  infm3  11263  prime  11720  raluz  11950  zsupss  11992  uzsupss  11995  xrsupsslem  12351  xrinfmsslem  12352  fz1sbc  12635  ssnn0fi  13004  fi1uzind  13492  brfi1indALT  13495  wrdind  13696  wrd2ind  13697  relexprelg  13997  rtrclreclem3  14019  relexpindlem  14022  relexpind  14023  rtrclind  14024  rexanre  14305  rexico  14312  limsupgle  14427  ello12  14466  ello12r  14467  ello1d  14473  elo12  14477  elo12r  14478  lo1resb  14514  o1resb  14516  rlimcn2  14540  addcn2  14543  mulcn2  14545  lo1le  14601  rpnnen2lem12  15170  sqrt2irr  15195  dfgcd2  15478  exprmfct  15629  isprm5  15632  isprm7  15633  prmdvdsexpr  15642  prmpwdvds  15821  vdwmc2  15896  ramtlecl  15917  ramub  15930  rami  15932  ramcl  15946  firest  16294  mreexexd  16509  acsfn  16520  prslem  17132  ispos  17148  posi  17151  isposd  17156  lubeldm  17182  lubval  17185  glbeldm  17195  glbval  17198  joinval2lem  17209  meetval2lem  17223  pospropd  17335  odlem1  18151  mndodcongi  18159  gexlem1  18191  sylow1lem3  18212  efgredlemb  18356  efgred  18358  frgpnabllem1  18473  isrrg  19493  mplsubglem  19639  mpllsslem  19640  ltbval  19676  opsrval  19679  xrsdsreclb  19997  islindf4  20384  mdetunilem1  20626  mdetunilem3  20628  mdetunilem4  20629  mdetunilem9  20634  chpscmat  20857  istopg  20910  isclo2  21103  neiptoptop  21146  neiptopnei  21147  lmbr  21273  ist0  21335  ist1-2  21362  t1sep2  21384  cmpfi  21422  2ndcdisj  21470  1stccn  21477  iskgen3  21563  ptpjopn  21626  hausdiag  21659  xkopt  21669  ist0-4  21743  isr0  21751  r0sep  21762  fbfinnfr  21855  fmfnfmlem2  21969  fmfnfmlem4  21971  fmfnfm  21972  cnflf  22016  cnfcf  22056  tmdgsum2  22110  tsmsf1o  22158  tsmsxplem1  22166  ustssel  22219  ustincl  22221  ustdiag  22222  ustinvel  22223  ustexhalf  22224  ust0  22233  ustuqtop4  22258  utopsnneiplem  22261  isucn2  22293  iducn  22297  metcnp  22556  txmetcnp  22562  metucn  22586  ngptgp  22650  nlmvscnlem1  22700  xrge0tsms  22847  xmetdcn2  22850  addcnlem  22877  ipcnlem1  23253  caucfil  23291  metcld  23314  metcld2  23315  ellimc2  23854  dvne0  23987  mdegleb  24037  mdegle0  24050  ply1divex  24109  fta1g  24140  dgrco  24244  plydivex  24265  fta1  24276  vieta1  24280  cxpcn3lem  24701  rlimcnp  24905  dvdsmulf1o  25133  ppiublem1  25140  dchrinv  25199  lgseisenlem2  25314  2sqlem6  25361  2sqlem8  25364  2sqlem10  25366  istrkgc  25566  istrkgb  25567  axtgcgrid  25575  axtg5seg  25577  axtgpasch  25579  axtgeucl  25584  tgcgr4  25639  axlowdimlem15  26049  usgr2wlkneq  26879  usgr2pthlem  26886  friendshipgt3  27585  isnvlem  27792  vacn  27876  smcnlem  27879  norm3lemt  28336  isch2  28407  chlimi  28418  omlsii  28589  eigorth  29024  stcltr1i  29460  elat2  29526  funcnv5mpt  29795  xrge0infss  29851  resspos  29983  xrge0tsmsd  30109  qqhucn  30360  esum2d  30479  eulerpartlemgvv  30762  sgn3da  30927  sgnnbi  30931  sgnpbi  30932  tgoldbachgt  31065  axtgupdim2OLD  31070  bnj1145  31382  bnj1171  31389  bnj1172  31390  erdszelem8  31501  mclsval  31781  mclsax  31787  mclsppslem  31801  climuzcnv  31885  elintfv  31982  poseq  32072  nocvxminlem  32212  ifscgr  32470  idinside  32510  brsegle  32534  trer  32629  filnetlem4  32695  bj-ssbjust  32932  bj-ssbequ  32943  bj-ssblem1  32944  bj-ssblem2  32945  bj-ssb1a  32946  bj-ssb1  32947  bj-ssbcom3lem  32963  bj-19.21t  33128  wl-sbrimt  33644  fin2so  33707  ptrecube  33720  poimirlem26  33746  poimirlem27  33747  heicant  33755  mbfresfi  33766  itg2addnc  33774  filbcmb  33845  sdclem2  33847  fdc  33850  fdc1  33851  rngoidmlem  34044  divrngidl  34136  pridlval  34141  smprngopr  34160  inecmo  34431  elcnvrefrels3  34592  ax12inda  34725  ax12v2-o  34726  isat3  35085  iscvlat2N  35102  psubspset  35522  ldilfset  35886  ldilset  35887  dilfsetN  35930  dilsetN  35931  cdlemefrs29bpre0  36174  cdlemefrs29clN  36177  cdlemefrs32fva  36178  cdlemn11pre  36988  dihord2pre  37003  lpolsetN  37260  aomclem8  38129  hbtlem5  38196  acsfn1p  38267  ifpbi1  38319  ifpbi12  38330  ifpbi13  38331  ntrneik2  38887  ntrneikb  38889  gneispacess2  38941  2sbc6g  39112  sbiota1  39131  uzwo4  39711  fsumiunss  40284  limsupre  40350  limsupref  40394  limsupbnd1f  40395  limsupmnf  40430  limsupre2  40434  limsupmnfuzlem  40435  limsupre2mpt  40439  limsupre3  40442  limsupre3mpt  40443  ioodvbdlimc1lem2  40624  ioodvbdlimc2lem  40626  dvmptfprodlem  40636  wallispilem3  40760  fourierdlem48  40847  sge0f1o  41075  sge0iunmptlemre  41108  sge0iunmpt  41111  vonioo  41375  vonicc  41378  bgoldbachlt  42273  tgoldbachlt  42276  sprsymrelfolem2  42308  ply1mulgsumlem1  42739  ply1mulgsumlem2  42740  elbigo2  42911  elbigo2r  42912  setrecseq  42997  setrec1lem1  42999  aacllem  43115