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

Theorem imbi2d 344
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 276 1 (𝜑 → ((𝜃𝜓) ↔ (𝜃𝜒)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209
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 210
This theorem is referenced by:  imbi12d  348  imbi2  352  pm5.42  547  orbi2d  913  19.23t  2212  axc14  2488  mojust  2623  mof  2648  eu6lem  2659  nfabdw  3003  2gencl  3521  3gencl  3522  vtocl2gf  3556  vtocl3gf  3557  vtocl2g  3558  vtocl2ga  3561  vtocl4g  3565  eqeu  3683  mo2icl  3691  euind  3701  reu7  3709  reuind  3730  sbctt  3828  reu8nf  3844  vtocl2dOLD  3914  sbcnestgfw  4353  sbcnestgf  4358  r19.36zv  4435  dedth2h  4507  dedth3h  4508  dedth4h  4509  reusngf  4597  reuprg0  4623  preq12bg  4768  elint  4868  elintrabg  4875  intab  4892  axrep1  5178  axreplem  5179  axrep2  5180  bm1.3ii  5193  reusv3  5294  pocl  5469  swopolem  5471  solin  5486  freq1  5513  frminex  5523  vtoclr  5603  2optocl  5634  3optocl  5635  raliunxp  5698  resieq  5853  iss  5892  cnveqb  6042  reu3op  6132  reuop  6133  preddowncl  6164  funmo  6361  funimaexg  6430  fnbrfvb  6711  fvelimab  6730  fvmptss  6773  fmptco  6884  fprg  6910  fnressn  6913  fressnfv  6915  isoselem  7089  ovg  7309  caovcan  7348  caovordig  7349  caovord  7355  tfisi  7569  tfindsg  7571  tfinds2  7574  tfinds3  7575  dfom2  7578  elom  7579  findsg  7606  finds2  7607  f1o2ndf1  7816  poxp  7820  fnse  7825  wfr3g  7951  wfrlem4  7956  smoeq  7985  smores  7987  smogt  8002  tfrlem1  8010  tfr3  8033  oaordi  8170  oeordi  8211  oeoa  8221  oeoe  8223  nnacl  8235  nnmcl  8236  nnecl  8237  nnacom  8241  nnaordi  8242  nnawordi  8245  nnaass  8246  nndi  8247  nnmass  8248  nnmsucr  8249  nnmcom  8250  nnmordi  8255  2ecoptocl  8386  3ecoptocl  8387  undifixp  8496  xpdom2g  8611  findcard2  8757  xpfi  8788  fnfi  8795  fodomfi  8796  finsschain  8830  marypha1lem  8896  marypha1  8897  supeq1  8908  ordiso2  8978  ordtypelem7  8987  wemaplem1  9009  inf3lem2  9091  inf3lem5  9094  infdiffi  9120  cantnfval2  9131  cantnfle  9133  cantnfp1lem3  9142  oemapval  9145  cantnflem1  9151  cantnf  9155  wemapwe  9159  cnfcom  9162  cnfcom3clem  9167  tz9.1  9170  r1pwALT  9274  cplem2  9318  karden  9323  updjud  9362  infxpenc2lem2  9446  fseqenlem1  9450  dfac8clem  9458  alephinit  9521  dfac4  9548  dfac5lem5  9553  dfac2a  9555  dfac2b  9556  dfacacn  9567  dfac12lem3  9571  kmlem2  9577  kmlem13  9588  ackbij1lem16  9657  sornom  9699  infpssrlem4  9728  fin23lem14  9755  fin23lem32  9766  fin23lem34  9768  fin23lem36  9770  isf32lem1  9775  isf32lem2  9776  axcc2lem  9858  axcc3  9860  axcclem  9879  zornn0g  9927  ttukeylem5  9935  ttukeylem6  9936  axrepnd  10016  axpowndlem3  10021  zfcndrep  10036  fpwwe2lem8  10059  pwfseqlem3  10082  wunr1om  10141  wunfi  10143  tskr1om  10189  ingru  10237  grudomon  10239  axgroth3  10253  axgroth4  10254  nqereu  10351  mulcanenq  10382  elnp  10409  elnpi  10410  prlem934  10455  infm3  11598  nnindd  11656  nnaddcl  11659  nnmulcl  11660  nnne0  11670  peano5uzi  12070  uzind2  12074  nn0indd  12078  zindd  12082  eluzadd  12272  uzaddcl  12303  uzwo  12310  indstr  12315  zmax  12344  xmulasslem  12677  xrsupsslem  12699  xrinfmsslem  12700  xrsupss  12701  xrinfmss  12702  flval2  13190  om2uzlti  13324  uzrdgfni  13332  rabssnn0fi  13360  mptnn0fsupp  13371  seqcl2  13395  seqfveq2  13399  seqshft2  13403  monoord  13407  seqsplit  13410  seqcaopr3  13412  seqf1olem2a  13415  seqf1o  13418  seqid2  13423  seqhomo  13424  ser1const  13433  expcllem  13447  expeq0  13466  mulexp  13475  expadd  13478  expmul  13481  expmordi  13538  leexp2r  13545  leexp1a  13546  bernneq  13597  modexp  13606  facdiv  13654  faclbnd  13657  faclbnd4lem4  13663  hashgadd  13745  hashxp  13802  hashmap  13803  hashf1lem2  13821  hashf1  13822  seqcoll  13829  wrdind  14086  wrd2ind  14087  pfxccatin12lem3  14096  cshweqrep  14185  2cshwcshw  14189  relexp0g  14383  relexpsucnnr  14386  relexpsucnnl  14393  relexpcnv  14396  relexpnndm  14402  relexpaddnn  14412  dfrtrclrec2  14418  rtrclreclem1  14419  rtrclreclem2  14420  rtrclreclem4  14422  dfrtrcl2  14423  relexpind  14425  reusq0  14824  rlim  14854  rlim2  14855  rlim0  14867  rlim0lt  14868  rlimi  14872  ello12r  14876  ello1mpt  14880  ello1d  14882  elo12r  14887  lo1o1  14891  o1lo1  14896  lo1res  14918  climshft  14935  o1compt  14946  rlimo1  14975  lo1add  14985  lo1mul  14986  rlimdiv  15004  climub  15020  climserle  15021  caucvgrlem  15031  caurcvgr  15032  iseraltlem2  15041  summolem2a  15074  sumss  15083  fsum2d  15128  fsumabs  15158  fsumrlim  15168  fsumo1  15169  fsumiun  15178  binom  15187  climcndslem1  15206  climcndslem2  15207  cvgrat  15241  clim2prod  15246  prodfn0  15252  prodfrec  15253  ntrivcvgfvn0  15257  prodmolem2a  15290  fprodabs  15330  fprodn0  15335  fprod2d  15337  binomfallfac  15397  bpolycl  15408  bpolydif  15411  fprodefsum  15450  demoivreALT  15556  ruclem8  15592  ruclem9  15593  dvdsle  15662  dvdsfac  15678  divalglem7  15750  bitsinv1  15791  sadcadd  15807  sadadd2  15809  saddisjlem  15813  smuval2  15831  smupvallem  15832  smu01lem  15834  smupval  15837  smueqlem  15839  smumullem  15841  bezoutlem4  15890  dfgcd2  15894  gcdmultipleOLD  15900  rplpwr  15907  nn0seqcvgd  15914  seq1st  15915  alginv  15919  algcvga  15923  algfx  15924  lcmf  15977  prmind2  16029  prmdvdsexp  16059  prmfac1  16063  reumodprminv  16141  pcmpt  16228  pcfac  16235  prmpwdvds  16240  prmreclem4  16255  vdwlem10  16326  ramval  16344  ramcl  16365  cshwrepswhash1  16438  prmlem1a  16442  imasleval  16816  ismre  16863  mreexexd  16921  lubprop  17598  lublecllem  17600  glbprop  17611  joinlem  17623  meetlem  17637  isglbd  17729  lubun  17735  poslubmo  17758  posglbmo  17759  poslubd  17760  mndind  17994  frmdgsum  18029  mulgnnass  18264  mhmmulg  18270  gsumwrev  18496  gsmsymgrfix  18558  gsmsymgreq  18562  psgnunilem3  18626  sylow1lem1  18725  efginvrel2  18855  efgsrel  18862  efgredlemd  18872  efgredlem  18875  efgred  18876  efgrelexlemb  18878  gsum2dlem2  19093  gsumcom2  19097  ablfac1eulem  19196  pgpfac1lem2  19199  pgpfac1lem5  19203  pgpfac1  19204  pgpfac  19208  srgmulgass  19283  srgpcomp  19284  srgbinom  19297  lmodvsmmulgdi  19671  isdomn2  20074  cnfldexp  20133  islindf4  20536  assamulgscm  20596  mplcoe1  20714  mplcoe3  20715  mplcoe5  20717  gsummoncoe1  20942  dmatval  21106  dmatel  21107  dmatmulcl  21114  pmatcoe1fsupp  21315  decpmataa0  21382  decpmatmulsumfsupp  21387  pmatcollpw2lem  21391  pm2mpmhmlem1  21432  fiinopn  21515  mretopd  21706  neiptoptop  21745  cnpfval  21848  iscnp3  21858  tgcn  21866  lmbr  21872  lmbr2  21873  lmbrf  21874  lmss  21912  ishaus  21936  hausnei2  21967  t1sep2  21983  fiuncmp  22018  dfconn2  22033  1stcfb  22059  2ndc1stc  22065  1stcrest  22067  1stcelcls  22075  1stccn  22077  lly1stc  22110  elkgen  22150  kgencn  22170  tx1stc  22264  xkopt  22269  cnmptcom  22292  isr0  22351  r0sep  22362  ptcmpfi  22427  isfildlem  22471  rnelfm  22567  fbflim  22590  flimrest  22597  isflf  22607  flffbas  22609  lmflf  22619  fclsrest  22638  isfcf  22648  cnextfvval  22679  tmdgsum  22709  eltsms  22747  tsmsi  22748  tsmsgsum  22753  tsmssubm  22757  tsmsres  22758  tsmsf1o  22759  isust  22818  isucn  22893  isucn2  22894  ucnima  22896  imasdsf1olem  22989  metss  23124  met1stc  23137  metcnp  23157  metcnpi  23160  metcnpi2  23161  metucn  23187  xrge0tsms  23448  fsumcn  23484  elcncf  23503  cncfi  23508  rescncf  23511  cncfco  23521  caucfil  23896  equivcau  23913  caubl  23921  caublcls  23922  ovolgelb  24093  ovolunlem1a  24109  ovolicc2lem3  24132  voliunlem1  24163  voliunlem3  24165  volsuplem  24168  volsup  24169  dyadmax  24211  vitali  24226  itg2leub  24347  itgfsum  24439  dvnadd  24541  dvnres  24543  cpnord  24547  dvnfre  24564  dvmptfsum  24587  dvferm1  24597  dvferm2  24599  rolle  24602  dvlip  24605  c1lip1  24609  lhop1  24626  deg1leb  24705  ply1divex  24746  fta1g  24777  plyco  24847  dgrcolem1  24879  dgrco  24881  dvnply2  24892  plydivex  24902  aalioulem2  24938  aalioulem3  24939  aalioulem5  24941  aaliou3lem2  24948  dvntaylp  24975  taylthlem1  24977  ulmdvlem3  25006  abelthlem9  25044  cxpmul2  25289  scvxcvx  25580  jensenlem2  25582  jensen  25583  wilthlem3  25664  perfectlem2  25823  bcmono  25870  bposlem5  25881  lgsquad2lem2  25978  addsq2reu  26033  2sqreulem1  26039  2sqreunnlem1  26042  dchrisumlem1  26082  dchrisum0flb  26103  pntpbnd1  26179  pntlemf  26198  qabvle  26218  qabvexp  26219  ostthlem2  26221  ostth2lem2  26227  tgcgr4  26334  usgr2pth  27562  wlkiswwlks2lem4  27667  wlkiswwlks2  27670  rusgrnumwwlk  27770  clwlkclwwlklem2a  27792  clwlkclwwlklem1  27793  clwlkclwwlkfo  27803  eupth2  28033  frgr3vlem1  28067  3vfriswmgrlem  28071  3vfriswmgr  28072  wlkl0  28161  numclwlk2lem2f1o  28173  isplig  28268  isnvlem  28402  nvi  28406  nmoubi  28564  nmounbi  28568  nmblolbi  28592  ipasslem1  28623  ipassi  28633  hlim2  28984  pjhth  29185  spansni  29349  elspansn2  29359  pjige0  29483  pjcjt2  29484  pjopyth  29512  elcnop  29649  elcnfn  29674  nmopub  29700  cnopc  29705  nmfnleub  29717  elnlfn  29720  cnfnc  29722  nmbdoplb  29817  nmcexi  29818  nmcoplb  29822  lnfnmul  29840  nmbdfnlb  29842  nmcfnlb  29846  pjss2coi  29956  pjssmi  29957  isst  30005  ishst  30006  stcltr1i  30066  mdbr  30086  dmdbr  30091  mddmd2  30101  mdslmd1lem3  30119  mdslmd1lem4  30120  elat2  30132  atcvat2  30181  cdj1i  30225  iuninc  30330  fmptcof2  30421  nn0min  30557  wrdt2ind  30648  ismnt  30686  xrge0tsmsd  30734  isomnd  30744  omndadd  30749  cyc3genpm  30836  isarchi2  30856  archirng  30859  archiexdiv  30861  archiabl  30869  isorng  30915  ofldchr  30930  mxidlval  31023  crefeq  31178  nexple  31353  esumfzf  31413  issiga  31456  isrnsiga  31457  isldsys  31500  ismeas  31543  isrnmeas  31544  measiun  31562  eulerpartlemn  31724  sseqp1  31738  rrvsum  31797  signsply0  31906  signstfvc  31929  bnj941  32129  bnj106  32225  bnj155  32236  bnj590  32267  bnj591  32268  bnj849  32282  bnj893  32285  bnj944  32295  bnj1128  32347  subfacp1lem6  32517  erdszelem8  32530  issconn  32558  cvmliftlem7  32623  cvmliftlem10  32626  cvmlift3lem2  32652  satfsschain  32696  satfrel  32699  satfdm  32701  satfrnmapom  32702  fmlafvel  32717  satffun  32741  mrsubvrs  32854  mclsssvlem  32894  mclsval  32895  mclsax  32901  mclsind  32902  shftvalg  33048  bccolsum  33056  iprodefisumlem  33057  faclimlem1  33060  dfpo2  33076  rdgprc  33124  trpredmintr  33155  frmin  33169  soseq  33181  frr3g  33206  fpr3g  33207  frrlem12  33219  fpr2  33225  frr2  33230  nosupno  33288  nosupdm  33289  nosupfv  33291  nosupres  33292  nosupbnd1lem1  33293  nosupbnd1lem3  33295  nosupbnd1lem5  33297  noeta  33307  fveleq  33884  unblimceq0  33931  bj-ax12  34075  bj-bm1.3ii  34453  rdgeqoa  34759  finxpreclem6  34785  domalom  34793  ralssiun  34796  wl-sblimt  34924  wl-sbhbt  34927  wl-2sb6d  34931  wl-mo2df  34943  wl-mo2t  34948  poimirlem2  35031  poimirlem25  35054  poimirlem28  35057  poimirlem31  35060  heicant  35064  mbfresfi  35075  itg2gt0cn  35084  sdclem2  35152  fdc  35155  seqpo  35157  incsequz  35158  mettrifi  35167  prdsbnd2  35205  heiborlem4  35224  bfplem1  35232  iscringd  35408  maxidlval  35449  igenval2  35476  iss2  35733  elrefrels3  35890  ax12eq  36209  ax12el  36210  ax12indalem  36213  ax12inda2ALT  36214  ax12inda  36216  ax12v2-o  36217  riotasvd  36224  isopos  36448  isat3  36575  ishlat1  36620  glbconN  36645  ispsubsp  37013  isldil  37378  isltrn  37387  isdilN  37422  trlval  37430  cdleme27b  37636  cdleme29b  37643  cdleme31sn1  37649  cdleme31sn1c  37656  cdleme40v  37737  cdlemk36  38181  cdlemkid5  38203  cdlemn11pre  38478  dihord2pre  38493  islpolN  38751  hdmapffval  39094  hdmapfval  39095  hdmapval2lem  39099  fzindd  39235  uzindd  39236  nnaddcom  39427  nnadddir  39429  nnmulcom  39431  ismrc  39586  incssnn0  39596  mzpexpmpt  39630  pell14qrexpclnn0  39751  monotuz  39826  rmxypos  39832  jm2.17a  39845  jm2.17b  39846  rmygeid  39849  jm2.18  39873  jm2.19lem3  39876  jm2.25  39884  jm2.15nn0  39888  jm2.16nn0  39889  wepwsolem  39930  aomclem8  39949  dfac11  39950  pwslnm  39982  lnr2i  40004  hbtlem5  40016  cnsrexpcl  40053  rngunsnply  40061  isdomn3  40092  ifpbi23  40125  elmapintrab  40220  elmapintab  40240  cnvcnvintabd  40244  eliunov2  40324  relexpxpnnidm  40348  relexpiidm  40349  relexpss1d  40350  iunrelexpmin1  40353  relexpmulnn  40354  iunrelexpmin2  40357  relexp0a  40361  trclimalb2  40371  clsk3nimkb  40690  ntrclsiso  40717  ntrclskb  40719  ntrneiiso  40741  ntrneix2  40743  ntrneixb  40745  gneispace2  40782  gneispacess2  40796  mnuunid  40933  dvgrat  40964  pm14.122b  41075  fnchoice  41606  fiiuncl  41647  ssinc  41673  ssdec  41674  wessf1ornlem  41763  dmrelrnrel  41808  fperiodmullem  41888  monoordxrv  42074  fmul01  42175  fmuldfeq  42178  climsuselem1  42202  climinff  42206  ellimcabssub0  42212  limcleqr  42239  addlimc  42243  0ellimcdiv  42244  limclner  42246  limsupref  42280  limsupub  42299  limsupmnf  42316  limsupre2lem  42319  limsupre2  42320  limsupre2mpt  42325  limsupre3lem  42327  limsupre3  42328  limsupre3mpt  42329  xlimbr  42422  cnrefiisplem  42424  dvnmptdivc  42533  dvnmptconst  42536  dvnmul  42538  iblspltprt  42568  itgspltprt  42574  stoweidlem2  42597  stoweidlem3  42598  stoweidlem17  42612  stoweidlem19  42614  stoweidlem21  42616  stoweidlem26  42621  fourierdlem42  42744  issal  42909  ismea  43043  isome  43086  carageniuncllem1  43113  caratheodorylem1  43118  2reu8i  43622  2reuimp0  43623  funressndmafv2rn  43732  2ffzoeq  43838  smonoord  43841  fargshiftf1  43911  ichnfimlem  43933  paireqne  43981  reupr  43992  reuopreuprim  43996  perfectALTVlem2  44193  lmodvsmdi  44737  dmatALTval  44762  dmatALTbasel  44764  snlindsntor  44833  ldepsnlinc  44870  elbigo2r  44920  elbigolo1  44924  itcovalt2  45044  setrecseq  45168  setrec2fun  45175  setrec2lem2  45177
  Copyright terms: Public domain W3C validator