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

Theorem imbi2d 331
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 264 1 (𝜑 → ((𝜃𝜓) ↔ (𝜃𝜒)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197
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 198
This theorem is referenced by:  imbi12d  335  imbi2  339  pm5.42  535  orbi2d  930  con3ALT  1098  axc15  2473  axc14  2533  mojust  2634  mof  2638  eu6  2645  2gencl  3441  3gencl  3442  vtocl2gf  3472  vtocl3gf  3473  vtocl4g  3481  eqeu  3584  mo2icl  3594  euind  3602  reu7  3610  reuind  3620  sbctt  3707  reu8nf  3722  sbcnestgf  4203  r19.36zv  4278  dedth2h  4347  dedth3h  4348  dedth4h  4349  preq12bg  4584  prel12gOLD  4585  elint  4686  elintrabg  4693  intab  4710  axrep1  4978  axreplem  4979  axrep2  4980  bm1.3ii  4991  reusv3  5087  pocl  5252  swopolem  5254  solin  5268  freq1  5294  frminex  5304  vtoclr  5380  2optocl  5412  3optocl  5413  raliunxp  5477  resieq  5625  iss  5666  cnveqb  5815  preddowncl  5934  funmo  6127  funimaexg  6196  fnbrfvb  6466  fvelimab  6484  fvmptss  6523  fmptco  6629  fprg  6656  fnressn  6659  fressnfv  6661  isoselem  6825  ovg  7039  caovcan  7078  caovordig  7079  caovord  7085  tfisi  7298  tfindsg  7300  tfinds2  7303  tfinds3  7304  dfom2  7307  elom  7308  findsg  7333  finds2  7334  f1o2ndf1  7529  poxp  7533  fnse  7538  wfr3g  7658  wfrlem4  7663  wfrlem4OLD  7664  smoeq  7693  smores  7695  smogt  7710  tfrlem1  7718  tfr3  7741  oaordi  7873  oeordi  7914  oeoa  7924  oeoe  7926  nnacl  7938  nnmcl  7939  nnecl  7940  nnacom  7944  nnaordi  7945  nnawordi  7948  nnaass  7949  nndi  7950  nnmass  7951  nnmsucr  7952  nnmcom  7953  nnmordi  7958  2ecoptocl  8083  3ecoptocl  8084  undifixp  8191  xpdom2g  8305  findcard2  8449  xpfi  8480  fnfi  8487  fodomfi  8488  finsschain  8522  marypha1lem  8588  marypha1  8589  supeq1  8600  ordiso2  8669  ordtypelem7  8678  wemaplem1  8700  inf3lem2  8783  inf3lem5  8786  infdiffi  8812  cantnfval2  8823  cantnfle  8825  cantnfp1lem3  8834  oemapval  8837  cantnflem1  8843  cantnf  8847  wemapwe  8851  cnfcom  8854  cnfcom3clem  8859  tz9.1  8862  r1pwALT  8966  cplem2  9010  karden  9015  updjud  9053  infxpenc2lem2  9136  fseqenlem1  9140  dfac8clem  9148  alephinit  9211  dfac4  9238  dfac5lem5  9243  dfac2a  9245  dfac2b  9246  dfac2OLD  9248  dfacacn  9258  dfac12lem3  9262  kmlem2  9268  kmlem13  9279  ackbij1lem16  9352  sornom  9394  infpssrlem4  9423  fin23lem14  9450  fin23lem32  9461  fin23lem34  9463  fin23lem36  9465  isf32lem1  9470  isf32lem2  9471  axcc2lem  9553  axcc3  9555  axcclem  9574  zornn0g  9622  ttukeylem5  9630  ttukeylem6  9631  axrepnd  9711  axpowndlem3  9716  zfcndrep  9731  fpwwe2lem8  9754  pwfseqlem3  9777  wunr1om  9836  wunfi  9838  tskr1om  9884  ingru  9932  grudomon  9934  axgroth3  9948  axgroth4  9949  nqereu  10046  mulcanenq  10077  elnp  10104  elnpi  10105  prlem934  10150  infm3  11277  nnaddcl  11339  nnmulcl  11340  nnmulclOLD  11341  peano5uzi  11752  uzind2  11756  nn0indd  11760  zindd  11764  eluzadd  11953  uzaddcl  11982  uzwo  11990  indstr  11995  zmax  12024  xmulasslem  12353  xrsupsslem  12375  xrinfmsslem  12376  xrsupss  12377  xrinfmss  12378  flval2  12859  om2uzlti  12993  uzrdgfni  13001  rabssnn0fi  13029  mptnn0fsupp  13040  seqcl2  13062  seqfveq2  13066  seqshft2  13070  monoord  13074  seqsplit  13077  seqcaopr3  13079  seqf1olem2a  13082  seqf1o  13085  seqid2  13090  seqhomo  13091  ser1const  13100  expcllem  13114  expeq0  13133  mulexp  13142  expadd  13145  expmul  13148  leexp2r  13161  leexp1a  13162  bernneq  13233  modexp  13242  facdiv  13314  faclbnd  13317  faclbnd4lem4  13323  faclbnd6  13326  hashgadd  13404  hashxp  13458  hashmap  13459  hashf1lem2  13477  hashf1  13478  seqcoll  13485  wrdind  13720  wrd2ind  13721  swrdccatin12lem3  13734  cshweqrep  13811  2cshwcshw  13815  relexp0g  14005  relexpsucnnr  14008  relexpsucnnl  14015  relexpcnv  14018  relexpnndm  14024  relexpaddnn  14034  dfrtrclrec2  14040  rtrclreclem1  14041  rtrclreclem2  14042  rtrclreclem4  14044  dfrtrcl2  14045  relexpind  14047  cjexp  14133  absexp  14287  rlim  14469  rlim2  14470  rlim0  14482  rlim0lt  14483  rlimi  14487  ello12r  14491  ello1mpt  14495  ello1d  14497  elo12r  14502  lo1o1  14506  o1lo1  14511  lo1res  14533  climshft  14550  o1compt  14561  rlimo1  14590  lo1add  14600  lo1mul  14601  rlimdiv  14619  climub  14635  climserle  14636  caucvgrlem  14646  caurcvgr  14647  iseraltlem2  14656  summolem2a  14689  sumss  14698  fsum2d  14745  fsumabs  14775  fsumrlim  14785  fsumo1  14786  fsumiun  14795  binom  14804  bcxmas  14809  climcndslem1  14823  climcndslem2  14824  cvgrat  14856  clim2prod  14861  prodfn0  14867  prodfrec  14868  ntrivcvgfvn0  14872  prodmolem2a  14905  fprodabs  14945  fprodn0  14950  fprod2d  14952  binomfallfac  15012  bpolycl  15023  bpolydif  15026  fprodefsum  15065  demoivreALT  15171  ruclem8  15206  ruclem9  15207  dvdsle  15275  dvdsfac  15291  divalglem7  15362  bitsinv1  15403  sadcadd  15419  sadadd2  15421  saddisjlem  15425  smuval2  15443  smupvallem  15444  smu01lem  15446  smupval  15449  smueqlem  15451  smumullem  15453  bezoutlem4  15498  dfgcd2  15502  gcdmultiple  15508  rplpwr  15515  nn0seqcvgd  15522  seq1st  15523  alginv  15527  algcvga  15531  algfx  15532  lcmf  15585  prmind2  15636  prmdvdsexp  15664  prmfac1  15668  reumodprminv  15746  pcmpt  15833  pcfac  15840  prmpwdvds  15845  prmreclem4  15860  vdwlem10  15931  ramval  15949  ramcl  15970  cshwrepswhash1  16041  prmlem1a  16045  imasleval  16426  ismre  16475  mreexexd  16533  lubprop  17211  lublecllem  17213  glbprop  17224  joinlem  17236  meetlem  17250  isglbd  17342  lubun  17348  poslubmo  17371  posglbmo  17372  poslubd  17373  mrcmndind  17591  frmdgsum  17624  mulgnnass  17799  mhmmulg  17805  gsumwrev  18017  gsmsymgrfix  18069  gsmsymgreq  18073  psgnunilem3  18137  sylow1lem1  18234  efginvrel2  18361  efgsrel  18368  efgredlemd  18378  efgredlem  18381  efgred  18382  efgrelexlemb  18384  gsum2dlem2  18591  gsumcom2  18595  ablfac1eulem  18693  pgpfac1lem2  18696  pgpfac1lem5  18700  pgpfac1  18701  pgpfac  18705  srgmulgass  18753  srgpcomp  18754  srgbinom  18767  lmodvsmmulgdi  19122  isdomn2  19528  assamulgscm  19579  mplcoe1  19694  mplcoe3  19695  mplcoe5  19697  gsummoncoe1  19902  cnfldexp  20007  islindf4  20408  dmatval  20530  dmatel  20531  dmatmulcl  20538  pmatcoe1fsupp  20740  decpmataa0  20807  decpmatmulsumfsupp  20812  pmatcollpw2lem  20816  pm2mpmhmlem1  20857  fiinopn  20940  mretopd  21131  neiptoptop  21170  cnpfval  21273  iscnp3  21283  tgcn  21291  lmbr  21297  lmbr2  21298  lmbrf  21299  lmss  21337  ishaus  21361  hausnei2  21392  t1sep2  21408  fiuncmp  21442  dfconn2  21457  1stcfb  21483  2ndc1stc  21489  1stcrest  21491  1stcelcls  21499  1stccn  21501  lly1stc  21534  elkgen  21574  kgencn  21594  tx1stc  21688  xkopt  21693  cnmptcom  21716  isr0  21775  r0sep  21786  ptcmpfi  21851  isfildlem  21895  rnelfm  21991  fbflim  22014  flimrest  22021  isflf  22031  flffbas  22033  lmflf  22043  fclsrest  22062  isfcf  22072  cnextfvval  22103  tmdmulg  22130  tmdgsum  22133  eltsms  22170  tsmsi  22171  tsmsgsum  22176  tsmssubm  22180  tsmsres  22181  tsmsf1o  22182  isust  22241  isucn  22316  isucn2  22317  ucnima  22319  imasdsf1olem  22412  metss  22547  met1stc  22560  metcnp  22580  metcnpi  22583  metcnpi2  22584  metucn  22610  xrge0tsms  22871  fsumcn  22907  elcncf  22926  cncfi  22931  rescncf  22934  cncfco  22944  caucfil  23315  equivcau  23332  caubl  23340  caublcls  23341  ovolgelb  23484  ovolunlem1a  23500  ovolicc2lem3  23523  voliunlem1  23554  voliunlem3  23556  volsuplem  23559  volsup  23560  dyadmax  23602  vitali  23617  itg2leub  23738  itgfsum  23830  dvnadd  23929  dvnres  23931  cpnord  23935  dvnfre  23952  dvmptfsum  23975  dvferm1  23985  dvferm2  23987  rolle  23990  dvlip  23993  c1lip1  23997  lhop1  24014  deg1leb  24092  ply1divex  24133  fta1g  24164  plyco  24234  dgrcolem1  24266  dgrco  24268  dvnply2  24279  plydivex  24289  aalioulem2  24325  aalioulem3  24326  aalioulem5  24328  aaliou3lem2  24335  dvntaylp  24362  taylthlem1  24364  ulmdvlem3  24393  abelthlem9  24431  cxpmul2  24672  scvxcvx  24949  jensenlem2  24951  jensen  24952  wilthlem3  25033  perfectlem2  25192  bcmono  25239  bposlem5  25250  lgsquad2lem2  25347  dchrisumlem1  25415  dchrisum0flb  25436  pntpbnd1  25512  pntlemf  25531  qabvle  25551  qabvexp  25552  ostthlem2  25554  ostth2lem2  25560  tgcgr4  25663  usgr2pth  26911  wlkiswwlks2lem4  27022  wlkiswwlks2  27025  rusgrnumwwlk  27140  clwlkclwwlklem2a  27164  clwlkclwwlklem1  27165  clwlkclwwlkfo  27175  clwlksfoclwwlkOLD  27260  eupth2  27435  frgr3vlem1  27471  3vfriswmgrlem  27475  3vfriswmgr  27476  wlkl0  27570  numclwlk2lem2f1o  27582  numclwlk2lem2f1oOLD  27589  isplig  27682  isnvlem  27816  nvi  27820  nmoubi  27978  nmounbi  27982  nmblolbi  28006  ipasslem1  28037  ipassi  28047  hlim2  28400  pjhth  28603  spansni  28767  elspansn2  28777  pjige0  28901  pjcjt2  28902  pjopyth  28930  elcnop  29067  elcnfn  29092  nmopub  29118  cnopc  29123  nmfnleub  29135  elnlfn  29138  cnfnc  29140  nmbdoplb  29235  nmcexi  29236  nmcoplb  29240  lnfnmul  29258  nmbdfnlb  29260  nmcfnlb  29264  pjss2coi  29374  pjssmi  29375  isst  29423  ishst  29424  stcltr1i  29484  mdbr  29504  dmdbr  29509  mddmd2  29519  mdslmd1lem3  29537  mdslmd1lem4  29538  elat2  29550  atcvat2  29599  cdj1i  29643  vtocl2d  29665  iuninc  29727  fmptcof2  29807  nnindd  29916  nn0min  29917  isomnd  30049  omndadd  30054  isarchi2  30087  archirng  30090  archiexdiv  30092  archiabl  30100  xrge0tsmsd  30133  isorng  30147  ofldchr  30162  crefeq  30260  nexple  30419  esumfzf  30479  issiga  30522  isrnsiga  30524  isldsys  30567  ismeas  30610  isrnmeas  30611  measiun  30629  eulerpartlemn  30791  sseqp1  30805  rrvsum  30864  signsply0  30976  signstfvc  30999  bnj941  31188  bnj106  31283  bnj155  31294  bnj590  31325  bnj591  31326  bnj849  31340  bnj893  31343  bnj944  31353  bnj1128  31403  subfacp1lem6  31512  erdszelem8  31525  issconn  31553  cvmliftlem7  31618  cvmliftlem10  31621  cvmlift3lem2  31647  mrsubvrs  31764  mclsssvlem  31804  mclsval  31805  mclsax  31811  mclsind  31812  shftvalg  31961  bccolsum  31969  iprodefisumlem  31970  faclimlem1  31973  dfpo2  31989  br1steqgOLD  32016  br2ndeqgOLD  32017  rdgprc  32042  trpredmintr  32073  frmin  32085  soseq  32097  frr3g  32122  nosupno  32192  nosupdm  32193  nosupfv  32195  nosupres  32196  nosupbnd1lem1  32197  nosupbnd1lem3  32199  nosupbnd1lem5  32201  noeta  32211  fveleq  32789  unblimceq0  32837  bj-axrep1  33121  bj-axrep2  33122  bj-axrep3  33123  bj-bm1.3ii  33353  rdgeqoa  33553  finxpreclem6  33568  wl-sblimt  33666  wl-sbhbt  33669  wl-2sb6d  33674  wl-mo2df  33685  wl-mo2t  33690  poimirlem2  33743  poimirlem25  33766  poimirlem28  33769  poimirlem31  33772  heicant  33776  mbfresfi  33787  itg2gt0cn  33796  sdclem2  33868  fdc  33871  seqpo  33873  incsequz  33874  mettrifi  33883  prdsbnd2  33924  heiborlem4  33943  bfplem1  33951  iscringd  34127  maxidlval  34168  igenval2  34195  iss2  34444  elrefrels3  34600  ax12eq  34739  ax12el  34740  ax12indalem  34743  ax12inda2ALT  34744  ax12inda  34746  ax12v2-o  34747  riotasvd  34754  isopos  34979  isat3  35106  ishlat1  35151  glbconN  35176  ispsubsp  35544  isldil  35909  isltrn  35918  isdilN  35953  trlval  35961  cdleme27b  36167  cdleme29b  36174  cdleme31sn1  36180  cdleme31sn1c  36187  cdleme40v  36268  cdlemk36  36712  cdlemkid5  36734  cdlemn11pre  37009  dihord2pre  37024  islpolN  37282  hdmapffval  37625  hdmapfval  37626  hdmapval2lem  37630  ismrc  37784  incssnn0  37794  mzpexpmpt  37828  pell14qrexpclnn0  37950  monotuz  38025  expmordi  38031  rmxypos  38033  jm2.17a  38046  jm2.17b  38047  rmygeid  38050  jm2.18  38074  jm2.19lem3  38077  jm2.25  38085  jm2.15nn0  38089  jm2.16nn0  38090  wepwsolem  38131  aomclem8  38150  dfac11  38151  pwslnm  38183  lnr2i  38205  hbtlem5  38217  cnsrexpcl  38254  rngunsnply  38262  isdomn3  38301  ifpbi23  38335  elmapintrab  38400  elmapintab  38420  cnvcnvintabd  38424  eliunov2  38489  relexpxpnnidm  38513  relexpiidm  38514  relexpss1d  38515  iunrelexpmin1  38518  relexpmulnn  38519  iunrelexpmin2  38522  relexp0a  38526  trclimalb2  38536  clsk3nimkb  38856  ntrclsiso  38883  ntrclskb  38885  ntrneiiso  38907  ntrneix2  38909  ntrneixb  38911  gneispace2  38948  gneispacess2  38962  dvgrat  39029  pm14.122b  39141  fnchoice  39700  fiiuncl  39745  ssinc  39775  ssdec  39776  wessf1ornlem  39878  dmrelrnrel  39924  fperiodmullem  40016  monoordxrv  40209  fmul01  40310  fmuldfeq  40313  climsuselem1  40337  climinff  40341  ellimcabssub0  40347  limcleqr  40374  addlimc  40378  0ellimcdiv  40379  limclner  40381  limsupref  40415  limsupub  40434  limsupmnf  40451  limsupre2lem  40454  limsupre2  40455  limsupre2mpt  40460  limsupre3lem  40462  limsupre3  40463  limsupre3mpt  40464  xlimbr  40551  cnrefiisplem  40553  dvnmptdivc  40651  dvnmptconst  40654  dvnmul  40656  iblspltprt  40686  itgspltprt  40692  stoweidlem2  40716  stoweidlem3  40717  stoweidlem17  40731  stoweidlem19  40733  stoweidlem21  40735  stoweidlem26  40740  fourierdlem42  40863  issal  41031  ismea  41165  isome  41208  carageniuncllem1  41235  caratheodorylem1  41240  funressndmafv2rn  41830  2ffzoeq  41931  smonoord  41934  fargshiftf1  41970  perfectALTVlem2  42224  lmodvsmdi  42749  dmatALTval  42775  dmatALTbasel  42777  snlindsntor  42846  ldepsnlinc  42883  elbigo2r  42933  elbigolo1  42937  setrecseq  43018  setrec2fun  43025  setrec2lem2  43027
  Copyright terms: Public domain W3C validator