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

Syntax hints:   → wi 4   ↔ wb 205

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 206

This theorem is referenced by:  imbi12d  344  imbi1  347  imim21b  394  pm5.33  832  con3ALT  1083  norasslem3  1536  sbjust  2069  sbequ  2089  sb6  2091  19.21t  2202  sb4b  2476  sb4bOLD  2477  drsb1  2500  ralcom2  3290  raleqf  3330  rspceaimv  3565  ralxpxfr2d  3576  alexeqg  3581  elab6g  3601  mo2icl  3652  sbc19.21g  3798  csbiebg  3869  ralss  3995  r19.37zv  4437  reuprg0  4643  intmin4  4913  ssexg  5250  pocl  5509  poclOLD  5510  vtoclr  5649  frsn  5673  fun11  6504  funimass4  6828  dff13  7122  f1mpt  7128  isopolem  7209  oprabidw  7299  oprabid  7300  caovcan  7467  caoftrn  7562  ordunisuc2  7679  tfisi  7693  tfinds  7694  tfindsg  7695  tfindsg2  7696  dfom2  7702  findsg  7733  frxp  7951  frrlem12  8097  dfsmo2  8162  qliftfun  8565  ecoptocl  8570  ecopovtrn  8583  dom2lem  8751  findcard  8911  findcard2  8912  ssfi  8921  findcard2OLD  9017  findcard3  9018  fiint  9052  supmo  9172  eqsup  9176  suplub  9180  supisoex  9194  infmo  9215  wemaplem1  9266  wemaplem2  9267  wemapsolem  9270  oemapvali  9403  cantnf  9412  wemapwe  9416  ttrclss  9439  karden  9637  aceq1  9857  zorn2lem1  10236  axrepndlem2  10333  axregndlem2  10343  pwfseqlem4  10402  gruurn  10538  indpi  10647  nqereu  10669  prcdnq  10733  supexpr  10794  ltsosr  10834  supsrlem  10851  supsr  10852  axpre-lttrn  10906  axpre-sup  10909  prodgt0  11805  infm3  11917  prime  12384  raluz  12618  zsupss  12659  uzsupss  12662  xrsupsslem  13023  xrinfmsslem  13024  fz1sbc  13314  ssnn0fi  13686  fi1uzind  14192  brfi1indALT  14195  wrdind  14416  wrd2ind  14417  relexprelg  14730  rtrclreclem3  14752  relexpindlem  14755  relexpind  14756  rtrclind  14757  rexanre  15039  rexico  15046  reusq0  15155  limsupgle  15167  ello12  15206  ello12r  15207  ello1d  15213  elo12  15217  elo12r  15218  lo1resb  15254  o1resb  15256  rlimcn3  15280  addcn2  15284  mulcn2  15286  lo1le  15344  rpnnen2lem12  15915  sqrt2irr  15939  dfgcd2  16235  exprmfct  16390  isprm5  16393  isprm7  16394  prmdvdsexpr  16403  prmpwdvds  16586  vdwmc2  16661  ramtlecl  16682  ramub  16695  rami  16697  ramcl  16711  firest  17124  mreexexd  17338  acsfn  17349  prslem  17997  ispos  18013  posi  18016  isposd  18022  pospropd  18026  lubeldm  18052  lubval  18055  glbeldm  18065  glbval  18068  joinval2lem  18079  meetval2lem  18093  odlem1  19124  mndodcongi  19132  gexlem1  19165  sylow1lem3  19186  efgredlemb  19333  efgred  19335  frgpnabllem1  19455  acsfn1p  20048  isrrg  20540  xrsdsreclb  20626  islindf4  21026  mplsubglem  21186  mpllsslem  21187  ltbval  21225  opsrval  21228  mdetunilem1  21742  mdetunilem3  21744  mdetunilem4  21745  mdetunilem9  21750  chpscmat  21972  istopg  22025  isclo2  22220  neiptoptop  22263  neiptopnei  22264  lmbr  22390  ist0  22452  ist1-2  22479  t1sep2  22501  cmpfi  22540  2ndcdisj  22588  1stccn  22595  iskgen3  22681  ptpjopn  22744  hausdiag  22777  xkopt  22787  ist0-4  22861  isr0  22869  r0sep  22880  fbfinnfr  22973  fmfnfmlem2  23087  fmfnfmlem4  23089  fmfnfm  23090  cnflf  23134  cnfcf  23174  tmdgsum2  23228  tsmsf1o  23277  tsmsxplem1  23285  ustssel  23338  ustincl  23340  ustdiag  23341  ustinvel  23342  ustexhalf  23343  ust0  23352  ustuqtop4  23377  utopsnneiplem  23380  isucn2  23412  iducn  23416  metcnp  23678  txmetcnp  23684  metucn  23708  ngptgp  23773  nlmvscnlem1  23831  xrge0tsms  23978  xmetdcn2  23981  addcnlem  24008  ipcnlem1  24390  caucfil  24428  metcld  24451  metcld2  24452  ellimc2  25022  dvne0  25156  mdegleb  25210  mdegle0  25223  ply1divex  25282  fta1g  25313  dgrco  25417  plydivex  25438  fta1  25449  vieta1  25453  cxpcn3lem  25881  rlimcnp  26096  dvdsmulf1o  26324  ppiublem1  26331  dchrinv  26390  lgseisenlem2  26505  2sqlem6  26552  2sqlem8  26555  2sqlem10  26557  istrkgc  26796  istrkgb  26797  axtgcgrid  26805  axtg5seg  26807  axtgpasch  26809  axtgeucl  26814  tgcgr4  26873  axlowdimlem15  27305  usgr2wlkneq  28103  usgr2pthlem  28110  friendshipgt3  28741  isnvlem  28951  vacn  29035  smcnlem  29038  norm3lemt  29493  isch2  29564  chlimi  29575  omlsii  29744  eigorth  30179  stcltr1i  30615  elat2  30681  funcnv5mpt  30984  xrge0infss  31062  wrdt2ind  31204  resspos  31223  xrge0tsmsd  31296  islinds5  31542  prmidlval  31591  ist0cld  31762  qqhucn  31921  esum2d  32040  eulerpartlemgvv  32322  sgn3da  32487  sgnnbi  32491  sgnpbi  32492  tgoldbachgt  32622  axtgupdim2ALTV  32627  bnj1145  32952  bnj1171  32959  bnj1172  32960  isacycgr1  33087  acycgrcycl  33088  erdszelem8  33139  satfrnmapom  33311  mclsval  33504  mclsax  33510  mclsppslem  33524  climuzcnv  33608  fnssintima  33655  elintfv  33717  xpord2ind  33773  xpord3ind  33779  poseq  33781  nocvxminlem  33951  ifscgr  34325  idinside  34365  brsegle  34389  trer  34484  filnetlem4  34549  bj-ssblem1  34814  bj-ssblem2  34815  bj-ax12  34817  bj-19.21t0  34992  mobidvALT  35020  currysetlem  35113  currysetlem1  35115  wl-sbrimt  35684  fin2so  35743  ptrecube  35756  poimirlem26  35782  poimirlem27  35783  heicant  35791  mbfresfi  35802  itg2addnc  35810  filbcmb  35877  sdclem2  35879  fdc  35882  fdc1  35883  rngoidmlem  36073  divrngidl  36165  pridlval  36170  smprngopr  36189  inecmo  36466  elcnvrefrels3  36628  ax12inda  36941  ax12v2-o  36942  isat3  37300  iscvlat2N  37317  psubspset  37737  ldilfset  38101  ldilset  38102  dilfsetN  38145  dilsetN  38146  cdlemefrs29bpre0  38389  cdlemefrs29clN  38392  cdlemefrs32fva  38393  cdlemn11pre  39203  dihord2pre  39218  lpolsetN  39475  sticksstones11  40092  sticksstones12a  40093  isdomn4  40152  fsuppind  40259  aomclem8  40866  hbtlem5  40933  ifpbi1  41046  ifpbi12  41057  ifpbi13  41058  ntrneik2  41655  ntrneikb  41657  gneispacess2  41709  2sbc6g  41986  sbiota1  42005  uzwo4  42554  fsumiunss  43070  limsupre  43136  limsupref  43180  limsupbnd1f  43181  limsupmnf  43216  limsupre2  43220  limsupmnfuzlem  43221  limsupre2mpt  43225  limsupre3  43228  limsupre3mpt  43229  ioodvbdlimc1lem2  43427  ioodvbdlimc2lem  43429  dvmptfprodlem  43439  wallispilem3  43562  fourierdlem48  43649  sge0f1o  43874  sge0iunmptlemre  43907  sge0iunmpt  43910  vonioo  44174  vonicc  44177  fcoresf1  44514  2reu8i  44556  2reuimp0  44557  2reuimp  44558  sprsymrelfolem2  44897  paireqne  44915  nfermltlrev  45148  bgoldbachlt  45217  tgoldbachlt  45220  ply1mulgsumlem1  45679  ply1mulgsumlem2  45680  elbigo2  45850  elbigo2r  45851  logic1  46088  postcposALT  46314  postc  46315  setrecseq  46343  setrec1lem1  46345  aacllem  46457