Theorem imbi1d 342

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 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  345  imbi1  348  imim21b  396  pm5.33  834  con3ALT  1085  norasslem3  1535  sbjust  2064  sbequ  2084  sb6  2086  19.21t  2197  sb4b  2473  sb4bOLD  2474  drsb1  2497  ralcom2  3308  raleqf  3344  rspceaimv  3570  ralxpxfr2d  3581  alexeqg  3586  elab6g  3605  mo2icl  3654  sbc19.21g  3799  csbiebg  3870  ralss  3996  r19.37zv  4438  reuprg0  4642  unissb  4879  intmin4  4915  dftr2c  5201  ssexg  5256  pocl  5521  poclOLD  5522  vtoclr  5661  frsn  5685  cotrg  6027  dffun2  6468  fun11  6537  funimass4  6866  dff13  7160  f1mpt  7166  isopolem  7248  oprabidw  7338  oprabid  7339  caovcan  7508  caoftrn  7603  ordunisuc2  7723  tfisi  7737  tfinds  7738  tfindsg  7739  tfindsg2  7740  dfom2  7746  findsg  7778  frxp  7998  frrlem12  8144  dfsmo2  8209  qliftfun  8622  ecoptocl  8627  ecopovtrn  8640  dom2lem  8813  findcard  8984  findcard2  8985  ssfi  8994  findcard2OLD  9100  findcard3  9101  fiint  9135  supmo  9255  eqsup  9259  suplub  9263  supisoex  9277  infmo  9298  wemaplem1  9349  wemaplem2  9350  wemapsolem  9353  oemapvali  9486  cantnf  9495  wemapwe  9499  ttrclss  9522  karden  9697  aceq1  9919  zorn2lem1  10298  axrepndlem2  10395  axregndlem2  10405  pwfseqlem4  10464  gruurn  10600  indpi  10709  nqereu  10731  prcdnq  10795  supexpr  10856  ltsosr  10896  supsrlem  10913  supsr  10914  axpre-lttrn  10968  axpre-sup  10971  prodgt0  11868  infm3  11980  prime  12447  raluz  12682  zsupss  12723  uzsupss  12726  xrsupsslem  13087  xrinfmsslem  13088  fz1sbc  13378  ssnn0fi  13751  fi1uzind  14256  brfi1indALT  14259  wrdind  14480  wrd2ind  14481  relexprelg  14794  rtrclreclem3  14816  relexpindlem  14819  relexpind  14820  rtrclind  14821  rexanre  15103  rexico  15110  reusq0  15219  limsupgle  15231  ello12  15270  ello12r  15271  ello1d  15277  elo12  15281  elo12r  15282  lo1resb  15318  o1resb  15320  rlimcn3  15344  addcn2  15348  mulcn2  15350  lo1le  15408  rpnnen2lem12  15979  sqrt2irr  16003  dfgcd2  16299  exprmfct  16454  isprm5  16457  isprm7  16458  prmdvdsexpr  16467  prmpwdvds  16650  vdwmc2  16725  ramtlecl  16746  ramub  16759  rami  16761  ramcl  16775  firest  17188  mreexexd  17402  acsfn  17413  prslem  18061  ispos  18077  posi  18080  isposd  18086  pospropd  18090  lubeldm  18116  lubval  18119  glbeldm  18129  glbval  18132  joinval2lem  18143  meetval2lem  18157  odlem1  19188  mndodcongi  19196  gexlem1  19229  sylow1lem3  19250  efgredlemb  19397  efgred  19399  frgpnabllem1  19519  acsfn1p  20112  isrrg  20604  xrsdsreclb  20690  islindf4  21090  mplsubglem  21250  mpllsslem  21251  ltbval  21289  opsrval  21292  mdetunilem1  21806  mdetunilem3  21808  mdetunilem4  21809  mdetunilem9  21814  chpscmat  22036  istopg  22089  isclo2  22284  neiptoptop  22327  neiptopnei  22328  lmbr  22454  ist0  22516  ist1-2  22543  t1sep2  22565  cmpfi  22604  2ndcdisj  22652  1stccn  22659  iskgen3  22745  ptpjopn  22808  hausdiag  22841  xkopt  22851  ist0-4  22925  isr0  22933  r0sep  22944  fbfinnfr  23037  fmfnfmlem2  23151  fmfnfmlem4  23153  fmfnfm  23154  cnflf  23198  cnfcf  23238  tmdgsum2  23292  tsmsf1o  23341  tsmsxplem1  23349  ustssel  23402  ustincl  23404  ustdiag  23405  ustinvel  23406  ustexhalf  23407  ust0  23416  ustuqtop4  23441  utopsnneiplem  23444  isucn2  23476  iducn  23480  metcnp  23742  txmetcnp  23748  metucn  23772  ngptgp  23837  nlmvscnlem1  23895  xrge0tsms  24042  xmetdcn2  24045  addcnlem  24072  ipcnlem1  24454  caucfil  24492  metcld  24515  metcld2  24516  ellimc2  25086  dvne0  25220  mdegleb  25274  mdegle0  25287  ply1divex  25346  fta1g  25377  dgrco  25481  plydivex  25502  fta1  25513  vieta1  25517  cxpcn3lem  25945  rlimcnp  26160  dvdsmulf1o  26388  ppiublem1  26395  dchrinv  26454  lgseisenlem2  26569  2sqlem6  26616  2sqlem8  26619  2sqlem10  26621  istrkgc  26860  istrkgb  26861  axtgcgrid  26869  axtg5seg  26871  axtgpasch  26873  axtgeucl  26878  tgcgr4  26937  axlowdimlem15  27369  usgr2wlkneq  28169  usgr2pthlem  28176  friendshipgt3  28807  isnvlem  29017  vacn  29101  smcnlem  29104  norm3lemt  29559  isch2  29630  chlimi  29641  omlsii  29810  eigorth  30245  stcltr1i  30681  elat2  30747  funcnv5mpt  31050  xrge0infss  31128  wrdt2ind  31270  resspos  31289  xrge0tsmsd  31362  islinds5  31608  prmidlval  31657  ist0cld  31828  qqhucn  31987  esum2d  32106  eulerpartlemgvv  32388  sgn3da  32553  sgnnbi  32557  sgnpbi  32558  tgoldbachgt  32688  axtgupdim2ALTV  32693  bnj1145  33018  bnj1171  33025  bnj1172  33026  isacycgr1  33153  acycgrcycl  33154  erdszelem8  33205  satfrnmapom  33377  mclsval  33570  mclsax  33576  mclsppslem  33590  climuzcnv  33674  fnssintima  33721  elintfv  33783  xpord2ind  33839  xpord3ind  33845  poseq  33847  nocvxminlem  34017  ifscgr  34391  idinside  34431  brsegle  34455  trer  34550  filnetlem4  34615  bj-ssblem1  34880  bj-ssblem2  34881  bj-ax12  34883  bj-19.21t0  35057  mobidvALT  35085  currysetlem  35178  currysetlem1  35180  wl-sbrimt  35749  fin2so  35808  ptrecube  35821  poimirlem26  35847  poimirlem27  35848  heicant  35856  mbfresfi  35867  itg2addnc  35875  filbcmb  35942  sdclem2  35944  fdc  35947  fdc1  35948  rngoidmlem  36138  divrngidl  36230  pridlval  36235  smprngopr  36254  inecmo  36529  elcnvrefrels3  36691  ax12inda  37004  ax12v2-o  37005  isat3  37363  iscvlat2N  37380  psubspset  37800  ldilfset  38164  ldilset  38165  dilfsetN  38208  dilsetN  38209  cdlemefrs29bpre0  38452  cdlemefrs29clN  38455  cdlemefrs32fva  38456  cdlemn11pre  39266  dihord2pre  39281  lpolsetN  39538  sticksstones11  40154  sticksstones12a  40155  isdomn4  40214  fsuppind  40316  aomclem8  40924  hbtlem5  40991  ifpbi1  41122  ifpbi12  41133  ifpbi13  41134  ntrneik2  41740  ntrneikb  41742  gneispacess2  41794  2sbc6g  42071  sbiota1  42090  uzwo4  42639  fsumiunss  43165  limsupre  43231  limsupref  43275  limsupbnd1f  43276  limsupmnf  43311  limsupre2  43315  limsupmnfuzlem  43316  limsupre2mpt  43320  limsupre3  43323  limsupre3mpt  43324  ioodvbdlimc1lem2  43522  ioodvbdlimc2lem  43524  dvmptfprodlem  43534  wallispilem3  43657  fourierdlem48  43744  sge0f1o  43970  sge0iunmptlemre  44003  sge0iunmpt  44006  vonioo  44270  vonicc  44273  fcoresf1  44621  2reu8i  44663  2reuimp0  44664  2reuimp  44665  sprsymrelfolem2  45003  paireqne  45021  nfermltlrev  45254  bgoldbachlt  45323  tgoldbachlt  45326  ply1mulgsumlem1  45785  ply1mulgsumlem2  45786  elbigo2  45956  elbigo2r  45957  logic1  46194  postcposALT  46420  postc  46421  setrecseq  46449  setrec1lem1  46451  aacllem  46563