Theorem imbi1d 344

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 251	. . 3 ⊢ (𝜑 → (𝜒 → 𝜓))
3	2	imim1d 83	. 2 ⊢ (𝜑 → ((𝜓 → 𝜃) → (𝜒 → 𝜃)))
4	1	biimpd 232	. . 3 ⊢ (𝜑 → (𝜓 → 𝜒))
5	4	imim1d 83	. 2 ⊢ (𝜑 → ((𝜒 → 𝜃) → (𝜓 → 𝜃)))
6	3, 5	impbid 215	1 ⊢ (𝜑 → ((𝜓 → 𝜃) ↔ (𝜒 → 𝜃)))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  imbi12d  347  imbi1  350  imim21b  400  pm5.33  849  con3ALT  1101  norasslem3  1566  sbjust  2098  sbequ  2120  sb6  2122  19.21t  2245  sb4b  2509  drsb1  2529  cbvralsvw  3318  sbralie  3344  raleqf  3347  ralcom2  3368  rmoeq1  3402  rspceaimv  3589  ralxpxfr2d  3607  alexeqg  3612  elab6g  3630  mo2icl  3679  sbc19.21g  3817  csbiebg  3886  ralss  4011  ralssOLD  4013  r19.37zv  4470  reuprg0  4670  unissb  4908  intmin4  4944  dftr2c  5223  ssexgOLD  5296  pocl  5579  vtoclr  5726  frsn  5751  cotrg  6113  dffun2  6550  fun11  6614  funimass4  6949  dff13  7254  f1mpt  7261  isopolem  7349  fnssintima  7368  oprabidw  7447  oprabid  7448  caovcan  7620  imaeqalov  7655  caoftrn  7721  ordunisuc2  7842  tfisi  7857  tfinds  7858  tfindsg  7859  tfindsg2  7860  dfom2  7866  findsg  7896  frxp  8124  xpord2indlem  8145  xpord3inddlem  8152  poseq  8156  frrlem12  8296  dfsmo2  8336  qliftfun  8802  ecoptocl  8807  ecopovtrn  8820  dom2lem  8991  findcard  9151  findcard2  9152  ssfi  9160  findcard3  9246  fiint  9289  supmo  9415  eqsup  9419  suplub  9423  supisoex  9438  infmo  9460  wemaplem1  9511  wemaplem2  9512  wemapsolem  9515  oemapvali  9656  cantnf  9665  wemapwe  9669  ttrclss  9692  kardenOLD  9892  aceq1  10113  zorn2lem1  10491  axrepndlem2  10589  axregndlem2  10599  gruurn  10794  indpi  10903  nqereu  10925  prcdnq  10989  supexpr  11050  ltsosr  11090  supsrlem  11107  supsr  11108  axpre-lttrn  11162  axpre-sup  11165  prodgt0  12073  infm3  12185  prime  12689  raluz  12932  zsupss  12973  uzsupss  12976  xrsupsslem  13345  xrinfmsslem  13346  fz1sbc  13641  ssnn0fi  14035  fi1uzind  14558  brfi1indALT  14561  wrdind  14777  wrd2ind  14778  relexprelg  15095  rtrclreclem3  15117  relexpindlem  15120  relexpind  15121  rtrclind  15122  sgn3da  15158  sgnnbi  15161  sgnpbi  15162  rexanre  15418  rexico  15425  reusq0  15536  limsupgle  15548  ello12  15587  ello12r  15588  ello1d  15594  elo12  15598  elo12r  15599  lo1resb  15635  o1resb  15637  rlimcn3  15661  addcn2  15665  mulcn2  15667  lo1le  15723  rpnnen2lem12  16299  sqrt2irr  16323  dfgcd2  16622  exprmfct  16781  isprm5  16784  isprm7  16785  prmdvdsexpr  16794  prmpwdvds  16982  vdwmc2  17057  ramtlecl  17078  ramub  17091  rami  17093  ramcl  17107  firest  17503  mreexexd  17722  acsfn  17733  prslem  18371  ispos  18388  posi  18391  isposd  18396  pospropd  18399  lubeldm  18425  lubval  18428  glbeldm  18438  glbval  18441  joinval2lem  18452  meetval2lem  18466  resspos  18503  odlem1  19629  mndodcongi  19637  gexlem1  19673  sylow1lem3  19694  efgredlemb  19840  efgred  19842  frgpnabllem1  19967  isrrg  20827  isdomn4  20844  domnlcanb  20848  domnrcanb  20850  acsfn1p  20932  prmidlval  21492  xrsdsreclb  21594  islindf4  22018  mplsubglem  22178  mpllsslem  22179  ltbval  22224  opsrval  22227  psdmul  22359  mdetunilem1  22799  mdetunilem3  22801  mdetunilem4  22802  mdetunilem9  22807  chpscmat  23029  istopg  23082  isclo2  23275  neiptoptop  23318  neiptopnei  23319  lmbr  23445  ist0  23507  ist1-2  23534  t1sep2  23556  cmpfi  23595  2ndcdisj  23644  1stccn  23651  iskgen3  23737  ptpjopn  23800  hausdiag  23833  xkopt  23843  ist0-4  23917  isr0  23925  r0sep  23936  fbfinnfr  24029  fmfnfmlem2  24143  fmfnfmlem4  24145  fmfnfm  24146  cnflf  24190  cnfcf  24230  tmdgsum2  24284  tsmsf1o  24333  tsmsxplem1  24341  ustssel  24394  ustincl  24396  ustdiag  24397  ustinvel  24398  ustexhalf  24399  ust0  24408  ustuqtop4  24432  utopsnneiplem  24435  isucn2  24466  iducn  24470  metcnp  24729  txmetcnp  24735  metucn  24759  ngptgp  24824  nlmvscnlem1  24874  xrge0tsms  25023  xmetdcn2  25026  addcnlem  25053  ipcnlem1  25435  caucfil  25473  metcld  25496  metcld2  25497  ellimc2  26067  dvne0  26201  mdegleb  26252  mdegle0  26265  ply1divex  26325  fta1g  26358  dgrco  26463  plydivex  26489  fta1  26500  vieta1  26504  cxpcn3lem  26943  rlimcnp  27161  mpodvdsmulf1o  27389  dvdsmulf1o  27391  ppiublem1  27397  dchrinv  27456  lgseisenlem2  27571  2sqlem6  27618  2sqlem8  27621  2sqlem10  27623  nocvxminlem  27978  addsprop  28200  leadds1  28213  negsprop  28259  mulsprop  28354  bdayons  28500  onsfi  28580  expsne0  28660  istrkgc  28754  istrkgb  28755  axtgcgrid  28763  axtg5seg  28765  axtgpasch  28767  axtgeucl  28772  tgcgr4  28831  axlowdimlem15  29337  usgr2wlkneq  30145  usgr2pthlem  30152  friendshipgt3  30796  isnvlem  31009  vacn  31093  smcnlem  31096  norm3lemt  31551  isch2  31622  chlimi  31633  omlsii  31802  eigorth  32237  stcltr1i  32673  elat2  32739  funcnv5mpt  33059  xrge0infss  33151  wrdt2ind  33315  xrge0tsmsd  33433  elrgspnlem4  33605  islinds5  33722  islbs5  33733  rprmdvdspow  33863  1arithufdlem3  33876  evl1deg1  33906  evl1deg2  33907  evl1deg3  33908  ply1dg1rt  33910  ist0cld  34263  qqhucn  34422  esum2d  34523  eulerpartlemgvv  34807  tgoldbachgt  35091  axtgupdim2ALTV  35096  bnj1145  35422  bnj1171  35429  bnj1172  35430  tz9.1regs  35580  isacycgr1  35651  acycgrcycl  35652  erdszelem8  35703  satfrnmapom  35875  mclsval  36068  mclsax  36074  mclsppslem  36088  climuzcnv  36176  elintfv  36270  ifscgr  36549  idinside  36589  brsegle  36613  ixpeq12dv  36761  trer  36860  filnetlem4  36925  axtcond  37022  axuntco  37023  dfttc4lem1  37072  mh-setindnd  37081  mh-unprimbi  37088  mh-regprimbi  37089  mh-infprim2bi  37091  bj-ssblem1  37309  bj-ssblem2  37310  bj-ax12  37312  bj-19.21t0  37498  mobidvALT  37525  currysetlem  37614  currysetlem1  37616  wl-ax12v2cl  38185  wl-sbrimt  38235  fin2so  38291  ptrecube  38304  poimirlem26  38330  poimirlem27  38331  heicant  38339  mbfresfi  38350  itg2addnc  38358  filbcmb  38424  sdclem2  38426  fdc  38429  fdc1  38430  rngoidmlem  38620  divrngidl  38712  pridlval  38717  smprngopr  38736  inecmo  39037  elcnvrefrels3  39297  eldisjdmqsim2  39498  qmapeldisjsim  39542  rnqmapeleldisjsim  39544  disjlem18  39585  ax12inda  39755  ax12v2-o  39756  isat3  40114  iscvlat2N  40131  psubspset  40551  ldilfset  40915  ldilset  40916  dilfsetN  40959  dilsetN  40960  cdlemefrs29bpre0  41203  cdlemefrs29clN  41206  cdlemefrs32fva  41207  cdlemn11pre  42017  dihord2pre  42032  lpolsetN  42289  isprimroot  42893  primrootsunit1  42897  primrootscoprbij  42902  aks6d1c1  42916  hashscontpow  42922  sticksstones11  42956  sticksstones12a  42957  aks6d1c6lem3  42972  fimgmcyc  43335  fsuppind  43355  aomclem8  43821  hbtlem5  43888  unielss  43978  ifpbi1  44236  ifpbi12  44247  ifpbi13  44248  ntrneik2  44851  ntrneikb  44853  gneispacess2  44905  2sbc6g  45158  sbiota1  45177  relpeq2  45687  nregmodel  45759  uzwo4  45806  iineq12dv  45857  fsumiunss  46324  limsupre  46388  limsupref  46432  limsupbnd1f  46433  limsupmnf  46468  limsupre2  46472  limsupmnfuzlem  46473  limsupre2mpt  46477  limsupre3  46480  limsupre3mpt  46481  ioodvbdlimc1lem2  46679  ioodvbdlimc2lem  46681  dvmptfprodlem  46691  wallispilem3  46814  fourierdlem48  46901  sge0f1o  47129  sge0iunmptlemre  47162  sge0iunmpt  47165  vonioo  47429  vonicc  47432  fcoresf1  47839  2reu8i  47883  2reuimp0  47884  2reuimp  47885  sprsymrelfolem2  48275  paireqne  48293  nfermltlrev  48542  bgoldbachlt  48611  tgoldbachlt  48614  gpgedgiov  48863  gpgedg2ov  48864  gpgedg2iv  48865  pgnbgreunbgrlem1  48911  pgnbgreunbgrlem3  48916  pgnbgreunbgrlem4  48917  pgnbgreunbgrlem6  48922  pgnbgreunbgr  48923  smprngprmrng  49137  ply1mulgsumlem1  49199  ply1mulgsumlem2  49200  elbigo2  49365  elbigo2r  49366  logic1  49602  postcposALT  50379  postc  50380  setrecseq  50496  setrec1lem1  50498  aacllem  50654