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

Syntax hints:   → wi 4   ↔ wb 206

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 207

This theorem is referenced by:  imbi12d  344  imbi1  347  imim21b  394  pm5.33  835  con3ALT  1084  norasslem3  1535  sbjust  2062  sbequ  2082  sb6  2084  19.21t  2205  sb4b  2478  drsb1  2498  cbvralsvw  3301  raleqf  3337  ralcom2  3361  rmoeq1  3400  rspceaimv  3612  ralxpxfr2d  3630  alexeqg  3635  elab6g  3653  mo2icl  3704  sbc19.21g  3844  csbiebg  3913  ralss  4040  ralssOLD  4042  r19.37zv  4484  reuprg0  4684  unissb  4921  intmin4  4959  dftr2c  5244  ssexg  5305  pocl  5582  vtoclr  5730  frsn  5755  cotrg  6109  dffun2  6552  fun11  6621  funimass4  6954  dff13  7258  f1mpt  7264  isopolem  7348  fnssintima  7365  oprabidw  7445  oprabid  7446  caovcan  7620  imaeqalov  7655  caoftrn  7721  ordunisuc2  7848  tfisi  7863  tfinds  7864  tfindsg  7865  tfindsg2  7866  dfom2  7872  findsg  7902  frxp  8134  xpord2indlem  8155  xpord3inddlem  8162  poseq  8166  frrlem12  8305  dfsmo2  8370  qliftfun  8825  ecoptocl  8830  ecopovtrn  8843  dom2lem  9015  findcard  9186  findcard2  9187  ssfi  9196  findcard3  9301  findcard3OLD  9302  fiint  9349  fiintOLD  9350  supmo  9475  eqsup  9479  suplub  9483  supisoex  9497  infmo  9518  wemaplem1  9569  wemaplem2  9570  wemapsolem  9573  oemapvali  9707  cantnf  9716  wemapwe  9720  ttrclss  9743  karden  9918  aceq1  10140  zorn2lem1  10519  axrepndlem2  10616  axregndlem2  10626  gruurn  10821  indpi  10930  nqereu  10952  prcdnq  11016  supexpr  11077  ltsosr  11117  supsrlem  11134  supsr  11135  axpre-lttrn  11189  axpre-sup  11192  prodgt0  12097  infm3  12210  prime  12683  raluz  12921  zsupss  12962  uzsupss  12965  xrsupsslem  13332  xrinfmsslem  13333  fz1sbc  13623  ssnn0fi  14009  fi1uzind  14529  brfi1indALT  14532  wrdind  14743  wrd2ind  14744  relexprelg  15060  rtrclreclem3  15082  relexpindlem  15085  relexpind  15086  rtrclind  15087  rexanre  15368  rexico  15375  reusq0  15484  limsupgle  15496  ello12  15535  ello12r  15536  ello1d  15542  elo12  15546  elo12r  15547  lo1resb  15583  o1resb  15585  rlimcn3  15609  addcn2  15613  mulcn2  15615  lo1le  15671  rpnnen2lem12  16244  sqrt2irr  16268  dfgcd2  16566  exprmfct  16724  isprm5  16727  isprm7  16728  prmdvdsexpr  16737  prmpwdvds  16925  vdwmc2  17000  ramtlecl  17021  ramub  17034  rami  17036  ramcl  17050  firest  17453  mreexexd  17667  acsfn  17678  prslem  18318  ispos  18335  posi  18338  isposd  18343  pospropd  18346  lubeldm  18372  lubval  18375  glbeldm  18385  glbval  18388  joinval2lem  18399  meetval2lem  18413  odlem1  19526  mndodcongi  19534  gexlem1  19570  sylow1lem3  19591  efgredlemb  19737  efgred  19739  frgpnabllem1  19864  isrrg  20671  isdomn4  20689  domnlcanb  20693  domnrcanb  20695  acsfn1p  20773  xrsdsreclb  21398  islindf4  21825  mplsubglem  21986  mpllsslem  21987  ltbval  22028  opsrval  22031  psdmul  22137  mdetunilem1  22585  mdetunilem3  22587  mdetunilem4  22588  mdetunilem9  22593  chpscmat  22815  istopg  22868  isclo2  23061  neiptoptop  23104  neiptopnei  23105  lmbr  23231  ist0  23293  ist1-2  23320  t1sep2  23342  cmpfi  23381  2ndcdisj  23429  1stccn  23436  iskgen3  23522  ptpjopn  23585  hausdiag  23618  xkopt  23628  ist0-4  23702  isr0  23710  r0sep  23721  fbfinnfr  23814  fmfnfmlem2  23928  fmfnfmlem4  23930  fmfnfm  23931  cnflf  23975  cnfcf  24015  tmdgsum2  24069  tsmsf1o  24118  tsmsxplem1  24126  ustssel  24179  ustincl  24181  ustdiag  24182  ustinvel  24183  ustexhalf  24184  ust0  24193  ustuqtop4  24218  utopsnneiplem  24221  isucn2  24252  iducn  24256  metcnp  24517  txmetcnp  24523  metucn  24547  ngptgp  24612  nlmvscnlem1  24662  xrge0tsms  24811  xmetdcn2  24814  addcnlem  24841  ipcnlem1  25234  caucfil  25272  metcld  25295  metcld2  25296  ellimc2  25867  dvne0  26005  mdegleb  26058  mdegle0  26071  ply1divex  26131  fta1g  26164  dgrco  26270  plydivex  26294  fta1  26305  vieta1  26309  cxpcn3lem  26745  rlimcnp  26963  mpodvdsmulf1o  27192  dvdsmulf1o  27194  ppiublem1  27201  dchrinv  27260  lgseisenlem2  27375  2sqlem6  27422  2sqlem8  27425  2sqlem10  27427  nocvxminlem  27777  addsprop  27964  sleadd1  27977  negsprop  28022  mulsprop  28111  expsne0  28369  istrkgc  28417  istrkgb  28418  axtgcgrid  28426  axtg5seg  28428  axtgpasch  28430  axtgeucl  28435  tgcgr4  28494  axlowdimlem15  28920  usgr2wlkneq  29723  usgr2pthlem  29730  friendshipgt3  30364  isnvlem  30576  vacn  30660  smcnlem  30663  norm3lemt  31118  isch2  31189  chlimi  31200  omlsii  31369  eigorth  31804  stcltr1i  32240  elat2  32306  funcnv5mpt  32625  xrge0infss  32711  wrdt2ind  32885  resspos  32902  xrge0tsmsd  33011  elrgspnlem4  33195  domnlcanOLD  33229  islinds5  33336  islbs5  33349  prmidlval  33406  rprmdvdspow  33502  1arithufdlem3  33515  evl1deg1  33542  evl1deg2  33543  evl1deg3  33544  ply1dg1rt  33545  ist0cld  33773  qqhucn  33934  esum2d  34035  eulerpartlemgvv  34319  sgn3da  34485  sgnnbi  34489  sgnpbi  34490  tgoldbachgt  34619  axtgupdim2ALTV  34624  bnj1145  34948  bnj1171  34955  bnj1172  34956  isacycgr1  35092  acycgrcycl  35093  erdszelem8  35144  satfrnmapom  35316  mclsval  35509  mclsax  35515  mclsppslem  35529  climuzcnv  35617  elintfv  35706  ifscgr  35986  idinside  36026  brsegle  36050  ixpeq12dv  36158  trer  36258  filnetlem4  36323  bj-ssblem1  36596  bj-ssblem2  36597  bj-ax12  36599  bj-19.21t0  36772  mobidvALT  36799  currysetlem  36887  currysetlem1  36889  wl-ax12v2cl  37448  wl-sbrimt  37489  fin2so  37555  ptrecube  37568  poimirlem26  37594  poimirlem27  37595  heicant  37603  mbfresfi  37614  itg2addnc  37622  filbcmb  37688  sdclem2  37690  fdc  37693  fdc1  37694  rngoidmlem  37884  divrngidl  37976  pridlval  37981  smprngopr  38000  inecmo  38297  elcnvrefrels3  38477  disjlem18  38742  ax12inda  38890  ax12v2-o  38891  isat3  39249  iscvlat2N  39266  psubspset  39687  ldilfset  40051  ldilset  40052  dilfsetN  40095  dilsetN  40096  cdlemefrs29bpre0  40339  cdlemefrs29clN  40342  cdlemefrs32fva  40343  cdlemn11pre  41153  dihord2pre  41168  lpolsetN  41425  isprimroot  42035  primrootsunit1  42039  primrootscoprbij  42044  aks6d1c1  42058  hashscontpow  42064  sticksstones11  42098  sticksstones12a  42099  aks6d1c6lem3  42114  fimgmcyc  42489  fsuppind  42545  aomclem8  43018  hbtlem5  43085  unielss  43175  ifpbi1  43435  ifpbi12  43446  ifpbi13  43447  ntrneik2  44050  ntrneikb  44052  gneispacess2  44104  2sbc6g  44379  sbiota1  44398  relpeq2  44911  uzwo4  45003  iineq12dv  45056  fsumiunss  45535  limsupre  45601  limsupref  45645  limsupbnd1f  45646  limsupmnf  45681  limsupre2  45685  limsupmnfuzlem  45686  limsupre2mpt  45690  limsupre3  45693  limsupre3mpt  45694  ioodvbdlimc1lem2  45892  ioodvbdlimc2lem  45894  dvmptfprodlem  45904  wallispilem3  46027  fourierdlem48  46114  sge0f1o  46342  sge0iunmptlemre  46375  sge0iunmpt  46378  vonioo  46642  vonicc  46645  fcoresf1  47027  2reu8i  47071  2reuimp0  47072  2reuimp  47073  sprsymrelfolem2  47426  paireqne  47444  nfermltlrev  47677  bgoldbachlt  47746  tgoldbachlt  47749  ply1mulgsumlem1  48249  ply1mulgsumlem2  48250  elbigo2  48419  elbigo2r  48420  logic1  48657  postcposALT  49161  postc  49162  setrecseq  49200  setrec1lem1  49202  aacllem  49316