MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  imbi2d Structured version   Visualization version   GIF version

Theorem imbi2d 329
Description: Deduction adding an antecedent to both sides of a logical equivalence. (Contributed by NM, 11-May-1993.)
Hypothesis
Ref Expression
imbid.1 (𝜑 → (𝜓𝜒))
Assertion
Ref Expression
imbi2d (𝜑 → ((𝜃𝜓) ↔ (𝜃𝜒)))

Proof of Theorem imbi2d
StepHypRef Expression
1 imbid.1 . . 3 (𝜑 → (𝜓𝜒))
21a1d 25 . 2 (𝜑 → (𝜃 → (𝜓𝜒)))
32pm5.74d 262 1 (𝜑 → ((𝜃𝜓) ↔ (𝜃𝜒)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196
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 197
This theorem is referenced by:  imbi12d  333  imbi2  337  pm5.42  572  orbi2d  740  con3ALT  1070  axc15  2448  axc14  2509  mo2  2616  2gencl  3376  3gencl  3377  vtocl2gf  3408  vtocl3gf  3409  vtocl4g  3417  eqeu  3518  mo2icl  3526  euind  3534  reu7  3542  reuind  3552  sbctt  3641  reu8nf  3657  sbcnestgf  4138  r19.36zv  4216  dedth2h  4284  dedth3h  4285  dedth4h  4286  preq12bg  4530  prel12gOLD  4531  elint  4633  elintrabg  4641  intab  4659  trssOLD  4914  axrep1  4924  axrep2  4925  axrep3  4926  bm1.3ii  4936  reusv3  5025  pocl  5194  swopolem  5196  solin  5210  freq1  5236  frminex  5246  vtoclr  5321  2optocl  5353  3optocl  5354  raliunxp  5417  resieq  5565  iss  5605  cnveqb  5748  preddowncl  5868  funmo  6065  funimaexg  6136  fnbrfvb  6397  fvelimab  6415  fvmptss  6454  fmptco  6559  fprg  6585  fnressn  6588  fressnfv  6590  isoselem  6754  ovg  6964  caovcan  7003  caovordig  7004  caovord  7010  tfisi  7223  tfindsg  7225  tfinds2  7228  tfinds3  7229  dfom2  7232  elom  7233  findsg  7258  finds2  7259  f1o2ndf1  7453  poxp  7457  fnse  7462  wfr3g  7582  wfrlem4  7587  smoeq  7616  smores  7618  smogt  7633  tfrlem1  7641  tfr3  7664  oaordi  7795  oeordi  7836  oeoa  7846  oeoe  7848  nnacl  7860  nnmcl  7861  nnecl  7862  nnacom  7866  nnaordi  7867  nnawordi  7870  nnaass  7871  nndi  7872  nnmass  7873  nnmsucr  7874  nnmcom  7875  nnmordi  7880  2ecoptocl  8005  3ecoptocl  8006  undifixp  8110  xpdom2g  8221  findcard2  8365  xpfi  8396  fnfi  8403  fodomfi  8404  finsschain  8438  marypha1lem  8504  marypha1  8505  supeq1  8516  ordiso2  8585  ordtypelem7  8594  wemaplem1  8616  inf3lem2  8699  inf3lem5  8702  infdiffi  8728  cantnfval2  8739  cantnfle  8741  cantnfp1lem3  8750  oemapval  8753  cantnflem1  8759  cantnf  8763  wemapwe  8767  cnfcom  8770  cnfcom3clem  8775  tz9.1  8778  r1pwALT  8882  cplem2  8926  karden  8931  infxpenc2lem2  9033  fseqenlem1  9037  dfac8clem  9045  alephinit  9108  dfac4  9135  dfac5lem5  9140  dfac2a  9142  dfac2b  9143  dfac2OLD  9145  dfacacn  9155  dfac12lem3  9159  kmlem2  9165  kmlem13  9176  ackbij1lem16  9249  sornom  9291  infpssrlem4  9320  fin23lem14  9347  fin23lem32  9358  fin23lem34  9360  fin23lem36  9362  isf32lem1  9367  isf32lem2  9368  axcc2lem  9450  axcc3  9452  axcclem  9471  zornn0g  9519  ttukeylem5  9527  ttukeylem6  9528  axrepnd  9608  axpowndlem3  9613  zfcndrep  9628  fpwwe2lem8  9651  pwfseqlem3  9674  wunr1om  9733  wunfi  9735  tskr1om  9781  ingru  9829  grudomon  9831  axgroth3  9845  axgroth4  9846  nqereu  9943  mulcanenq  9974  elnp  10001  elnpi  10002  prlem934  10047  infm3  11174  nnaddcl  11234  nnmulcl  11235  peano5uzi  11658  uzind2  11662  nn0indd  11666  zindd  11670  eluzadd  11908  uzaddcl  11937  uzwo  11944  indstr  11949  zmax  11978  xmulasslem  12308  xrsupsslem  12330  xrinfmsslem  12331  xrsupss  12332  xrinfmss  12333  flval2  12809  om2uzlti  12943  uzrdgfni  12951  rabssnn0fi  12979  mptnn0fsupp  12991  seqcl2  13013  seqfveq2  13017  seqshft2  13021  monoord  13025  seqsplit  13028  seqcaopr3  13030  seqf1olem2a  13033  seqf1o  13036  seqid2  13041  seqhomo  13042  ser1const  13051  expcllem  13065  expeq0  13084  mulexp  13093  expadd  13096  expmul  13099  leexp2r  13112  leexp1a  13113  bernneq  13184  modexp  13193  facdiv  13268  faclbnd  13271  faclbnd4lem4  13277  faclbnd6  13280  hashgadd  13358  hashxp  13413  hashmap  13414  hashf1lem2  13432  hashf1  13433  seqcoll  13440  wrdind  13676  wrd2ind  13677  swrdccatin12lem3  13690  cshweqrep  13767  2cshwcshw  13771  relexp0g  13961  relexpsucnnr  13964  relexpsucnnl  13971  relexpcnv  13974  relexpnndm  13980  relexpaddnn  13990  dfrtrclrec2  13996  rtrclreclem1  13997  rtrclreclem2  13998  rtrclreclem4  14000  dfrtrcl2  14001  relexpind  14003  cjexp  14089  absexp  14243  rlim  14425  rlim2  14426  rlim0  14438  rlim0lt  14439  rlimi  14443  ello12r  14447  ello1mpt  14451  ello1d  14453  elo12r  14458  lo1o1  14462  o1lo1  14467  lo1res  14489  climshft  14506  o1compt  14517  rlimo1  14546  lo1add  14556  lo1mul  14557  rlimdiv  14575  climub  14591  climserle  14592  caucvgrlem  14602  caurcvgr  14603  iseraltlem2  14612  summolem2a  14645  sumss  14654  fsum2d  14701  fsumabs  14732  fsumrlim  14742  fsumo1  14743  fsumiun  14752  binom  14761  bcxmas  14766  climcndslem1  14780  climcndslem2  14781  cvgrat  14814  clim2prod  14819  prodfn0  14825  prodfrec  14826  ntrivcvgfvn0  14830  prodmolem2a  14863  fprodabs  14903  fprodn0  14908  fprod2d  14910  binomfallfac  14971  bpolycl  14982  bpolydif  14985  fprodefsum  15024  demoivreALT  15130  ruclem8  15165  ruclem9  15166  dvdsle  15234  dvdsfac  15250  divalglem7  15324  bitsinv1  15366  sadcadd  15382  sadadd2  15384  saddisjlem  15388  smuval2  15406  smupvallem  15407  smu01lem  15409  smupval  15412  smueqlem  15414  smumullem  15416  bezoutlem4  15461  dfgcd2  15465  gcdmultiple  15471  rplpwr  15478  nn0seqcvgd  15485  seq1st  15486  alginv  15490  algcvga  15494  algfx  15495  lcmf  15548  prmind2  15600  prmdvdsexp  15629  prmfac1  15633  reumodprminv  15711  pcmpt  15798  pcfac  15805  prmpwdvds  15810  prmreclem4  15825  vdwlem10  15896  ramval  15914  ramcl  15935  cshwrepswhash1  16011  prmlem1a  16015  imasleval  16403  ismre  16452  mreexexd  16510  lubprop  17187  lublecllem  17189  glbprop  17200  joinlem  17212  meetlem  17226  isglbd  17318  lubun  17324  poslubmo  17347  posglbmo  17348  poslubd  17349  mrcmndind  17567  frmdgsum  17600  mulgnnass  17777  mulgnnassOLD  17778  mhmmulg  17784  gsumwrev  17996  gsmsymgrfix  18048  gsmsymgreq  18052  psgnunilem3  18116  sylow1lem1  18213  efginvrel2  18340  efgsrel  18347  efgredlemd  18357  efgredlem  18360  efgred  18361  efgrelexlemb  18363  gsum2dlem2  18570  gsumcom2  18574  ablfac1eulem  18671  pgpfac1lem2  18674  pgpfac1lem5  18678  pgpfac1  18679  pgpfac  18683  srgmulgass  18731  srgpcomp  18732  srgbinom  18745  lmodvsmmulgdi  19100  isdomn2  19501  assamulgscm  19552  mplcoe1  19667  mplcoe3  19668  mplcoe5  19670  gsummoncoe1  19876  cnfldexp  19981  islindf4  20379  dmatval  20500  dmatel  20501  dmatmulcl  20508  pmatcoe1fsupp  20708  decpmataa0  20775  decpmatmulsumfsupp  20780  pmatcollpw2lem  20784  pm2mpmhmlem1  20825  fiinopn  20908  mretopd  21098  neiptoptop  21137  cnpfval  21240  iscnp3  21250  tgcn  21258  lmbr  21264  lmbr2  21265  lmbrf  21266  lmss  21304  ishaus  21328  hausnei2  21359  t1sep2  21375  fiuncmp  21409  dfconn2  21424  1stcfb  21450  2ndc1stc  21456  1stcrest  21458  1stcelcls  21466  1stccn  21468  lly1stc  21501  elkgen  21541  kgencn  21561  tx1stc  21655  xkopt  21660  cnmptcom  21683  isr0  21742  r0sep  21753  ptcmpfi  21818  isfildlem  21862  rnelfm  21958  fbflim  21981  flimrest  21988  isflf  21998  flffbas  22000  lmflf  22010  fclsrest  22029  isfcf  22039  cnextfvval  22070  tmdmulg  22097  tmdgsum  22100  eltsms  22137  tsmsi  22138  tsmsgsum  22143  tsmssubm  22147  tsmsres  22148  tsmsf1o  22149  isust  22208  isucn  22283  isucn2  22284  ucnima  22286  imasdsf1olem  22379  metss  22514  met1stc  22527  metcnp  22547  metcnpi  22550  metcnpi2  22551  metucn  22577  xrge0tsms  22838  fsumcn  22874  elcncf  22893  cncfi  22898  rescncf  22901  cncfco  22911  caucfil  23281  equivcau  23298  caubl  23306  caublcls  23307  ovolgelb  23448  ovolunlem1a  23464  ovolicc2lem3  23487  voliunlem1  23518  voliunlem3  23520  volsuplem  23523  volsup  23524  dyadmax  23566  vitali  23581  itg2leub  23700  itgfsum  23792  dvnadd  23891  dvnres  23893  cpnord  23897  dvnfre  23914  dvmptfsum  23937  dvferm1  23947  dvferm2  23949  rolle  23952  dvlip  23955  c1lip1  23959  lhop1  23976  deg1leb  24054  ply1divex  24095  fta1g  24126  plyco  24196  dgrcolem1  24228  dgrco  24230  dvnply2  24241  plydivex  24251  aalioulem2  24287  aalioulem3  24288  aalioulem5  24290  aaliou3lem2  24297  dvntaylp  24324  taylthlem1  24326  ulmdvlem3  24355  abelthlem9  24393  cxpmul2  24634  scvxcvx  24911  jensenlem2  24913  jensen  24914  wilthlem3  24995  perfectlem2  25154  bcmono  25201  bposlem5  25212  lgsquad2lem2  25309  dchrisumlem1  25377  dchrisum0flb  25398  pntpbnd1  25474  pntlemf  25493  qabvle  25513  qabvexp  25514  ostthlem2  25516  ostth2lem2  25522  tgcgr4  25625  usgr2pth  26870  wlkiswwlks2lem4  26981  wlkiswwlks2  26984  rusgrnumwwlk  27097  clwlkclwwlklem2a  27121  clwlkclwwlklem1  27122  clwlkclwwlkfo  27132  clwlksfoclwwlkOLD  27217  eupth2  27391  frgr3vlem1  27427  3vfriswmgrlem  27431  3vfriswmgr  27432  wlkl0  27528  numclwlk2lem2f1o  27540  numclwlk2lem2f1oOLD  27547  isplig  27639  isnvlem  27774  nvi  27778  nmoubi  27936  nmounbi  27940  nmblolbi  27964  ipasslem1  27995  ipassi  28005  hlim2  28358  pjhth  28561  spansni  28725  elspansn2  28735  pjige0  28859  pjcjt2  28860  pjopyth  28888  elcnop  29025  elcnfn  29050  nmopub  29076  cnopc  29081  nmfnleub  29093  elnlfn  29096  cnfnc  29098  nmbdoplb  29193  nmcexi  29194  nmcoplb  29198  lnfnmul  29216  nmbdfnlb  29218  nmcfnlb  29222  pjss2coi  29332  pjssmi  29333  isst  29381  ishst  29382  stcltr1i  29442  mdbr  29462  dmdbr  29467  mddmd2  29477  mdslmd1lem3  29495  mdslmd1lem4  29496  elat2  29508  atcvat2  29557  cdj1i  29601  vtocl2d  29623  iuninc  29686  fmptcof2  29766  nnindd  29875  nn0min  29876  isomnd  30010  omndadd  30015  isarchi2  30048  archirng  30051  archiexdiv  30053  archiabl  30061  xrge0tsmsd  30094  isorng  30108  ofldchr  30123  crefeq  30221  nexple  30380  esumfzf  30440  issiga  30483  isrnsiga  30485  isldsys  30528  ismeas  30571  isrnmeas  30572  measiun  30590  eulerpartlemn  30752  sseqp1  30766  rrvsum  30825  signsply0  30937  signstfvc  30960  bnj941  31150  bnj106  31245  bnj155  31256  bnj590  31287  bnj591  31288  bnj849  31302  bnj893  31305  bnj944  31315  bnj1128  31365  subfacp1lem6  31474  erdszelem8  31487  issconn  31515  cvmliftlem7  31580  cvmliftlem10  31583  cvmlift3lem2  31609  mrsubvrs  31726  mclsssvlem  31766  mclsval  31767  mclsax  31773  mclsind  31774  shftvalg  31924  bccolsum  31932  iprodefisumlem  31933  faclimlem1  31936  dfpo2  31952  br1steqgOLD  31979  br2ndeqgOLD  31980  rdgprc  32005  trpredmintr  32036  frmin  32048  soseq  32060  frr3g  32085  nosupno  32155  nosupdm  32156  nosupfv  32158  nosupres  32159  nosupbnd1lem1  32160  nosupbnd1lem3  32162  nosupbnd1lem5  32164  noeta  32174  fveleq  32756  unblimceq0  32804  bj-axrep1  33094  bj-axrep2  33095  bj-axrep3  33096  rdgeqoa  33529  finxpreclem6  33544  wl-sblimt  33645  wl-sbhbt  33648  wl-2sb6d  33654  wl-mo2df  33665  wl-mo2t  33670  poimirlem2  33724  poimirlem25  33747  poimirlem28  33750  poimirlem31  33753  heicant  33757  mbfresfi  33769  itg2gt0cn  33778  sdclem2  33851  fdc  33854  seqpo  33856  incsequz  33857  mettrifi  33866  prdsbnd2  33907  heiborlem4  33926  bfplem1  33934  iscringd  34110  maxidlval  34151  igenval2  34178  iss2  34435  elrefrels3  34591  ax12eq  34730  ax12el  34731  ax12indalem  34734  ax12inda2ALT  34735  ax12inda  34737  ax12v2-o  34738  riotasvd  34745  isopos  34970  isat3  35097  ishlat1  35142  glbconN  35166  ispsubsp  35534  isldil  35899  isltrn  35908  isdilN  35944  trlval  35952  cdleme27b  36158  cdleme29b  36165  cdleme31sn1  36171  cdleme31sn1c  36178  cdleme40v  36259  cdlemk36  36703  cdlemkid5  36725  cdlemn11pre  37001  dihord2pre  37016  islpolN  37274  hdmapffval  37620  hdmapfval  37621  hdmapval2lem  37625  ismrc  37766  incssnn0  37776  mzpexpmpt  37810  pell14qrexpclnn0  37932  monotuz  38008  expmordi  38014  rmxypos  38016  jm2.17a  38029  jm2.17b  38030  rmygeid  38033  jm2.18  38057  jm2.19lem3  38060  jm2.25  38068  jm2.15nn0  38072  jm2.16nn0  38073  wepwsolem  38114  aomclem8  38133  dfac11  38134  pwslnm  38166  lnr2i  38188  hbtlem5  38200  cnsrexpcl  38237  rngunsnply  38245  isdomn3  38284  ifpbi23  38319  elmapintrab  38384  elmapintab  38404  cnvcnvintabd  38408  eliunov2  38473  relexpxpnnidm  38497  relexpiidm  38498  relexpss1d  38499  iunrelexpmin1  38502  relexpmulnn  38503  iunrelexpmin2  38506  relexp0a  38510  trclimalb2  38520  clsk3nimkb  38840  ntrclsiso  38867  ntrclskb  38869  ntrneiiso  38891  ntrneix2  38893  ntrneixb  38895  gneispace2  38932  gneispacess2  38946  dvgrat  39013  pm14.122b  39126  fnchoice  39687  fiiuncl  39733  ssinc  39763  ssdec  39764  wessf1ornlem  39870  dmrelrnrel  39918  fperiodmullem  40016  monoordxrv  40210  fmul01  40315  fmuldfeq  40318  climsuselem1  40342  climinff  40346  ellimcabssub0  40352  limcleqr  40379  addlimc  40383  0ellimcdiv  40384  limclner  40386  limsupref  40420  limsupub  40439  limsupmnf  40456  limsupre2lem  40459  limsupre2  40460  limsupre2mpt  40465  limsupre3lem  40467  limsupre3  40468  limsupre3mpt  40469  xlimbr  40556  cnrefiisplem  40558  dvnmptdivc  40656  dvnmptconst  40659  dvnmul  40661  iblspltprt  40692  itgspltprt  40698  stoweidlem2  40722  stoweidlem3  40723  stoweidlem17  40737  stoweidlem19  40739  stoweidlem21  40741  stoweidlem26  40746  fourierdlem42  40869  issal  41037  ismea  41171  isome  41214  carageniuncllem1  41241  caratheodorylem1  41246  2ffzoeq  41848  smonoord  41851  fargshiftf1  41887  perfectALTVlem2  42141  lmodvsmdi  42673  dmatALTval  42699  dmatALTbasel  42701  snlindsntor  42770  ldepsnlinc  42807  elbigo2r  42857  elbigolo1  42861  setrecseq  42942  setrec2fun  42949  setrec2lem2  42951
  Copyright terms: Public domain W3C validator