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

Theorem imbi2d 342
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 274 1 (𝜑 → ((𝜃𝜓) ↔ (𝜃𝜒)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207
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 208
This theorem is referenced by:  imbi12d  346  imbi2  350  pm5.42  544  orbi2d  909  con3ALTOLD  1077  19.23t  2201  axc15OLD  2439  axc14  2481  mojust  2617  mof  2643  eu6lem  2654  nfabdw  3000  2gencl  3536  3gencl  3537  vtocl2gf  3570  vtocl3gf  3571  vtocl2g  3572  vtocl2ga  3575  vtocl4g  3579  eqeu  3696  mo2icl  3704  euind  3714  reu7  3722  reuind  3743  sbctt  3843  reu8nf  3859  vtocl2dOLD  3930  sbcnestgfw  4369  sbcnestgf  4374  r19.36zv  4450  dedth2h  4522  dedth3h  4523  dedth4h  4524  reusngf  4606  reuprg0  4632  preq12bg  4778  elint  4875  elintrabg  4882  intab  4899  axrep1  5183  axreplem  5184  axrep2  5185  bm1.3ii  5198  reusv3  5297  pocl  5475  swopolem  5477  solin  5492  freq1  5519  frminex  5529  vtoclr  5609  2optocl  5640  3optocl  5641  raliunxp  5704  resieq  5858  iss  5897  cnveqb  6047  reu3op  6137  reuop  6138  preddowncl  6169  funmo  6365  funimaexg  6434  fnbrfvb  6712  fvelimab  6731  fvmptss  6773  fmptco  6884  fprg  6910  fnressn  6913  fressnfv  6915  isoselem  7083  ovg  7302  caovcan  7341  caovordig  7342  caovord  7348  tfisi  7561  tfindsg  7563  tfinds2  7566  tfinds3  7567  dfom2  7570  elom  7571  findsg  7597  finds2  7598  f1o2ndf1  7809  poxp  7813  fnse  7818  wfr3g  7944  wfrlem4  7949  smoeq  7978  smores  7980  smogt  7995  tfrlem1  8003  tfr3  8026  oaordi  8162  oeordi  8203  oeoa  8213  oeoe  8215  nnacl  8227  nnmcl  8228  nnecl  8229  nnacom  8233  nnaordi  8234  nnawordi  8237  nnaass  8238  nndi  8239  nnmass  8240  nnmsucr  8241  nnmcom  8242  nnmordi  8247  2ecoptocl  8378  3ecoptocl  8379  undifixp  8487  xpdom2g  8602  findcard2  8747  xpfi  8778  fnfi  8785  fodomfi  8786  finsschain  8820  marypha1lem  8886  marypha1  8887  supeq1  8898  ordiso2  8968  ordtypelem7  8977  wemaplem1  8999  inf3lem2  9081  inf3lem5  9084  infdiffi  9110  cantnfval2  9121  cantnfle  9123  cantnfp1lem3  9132  oemapval  9135  cantnflem1  9141  cantnf  9145  wemapwe  9149  cnfcom  9152  cnfcom3clem  9157  tz9.1  9160  r1pwALT  9264  cplem2  9308  karden  9313  updjud  9352  infxpenc2lem2  9435  fseqenlem1  9439  dfac8clem  9447  alephinit  9510  dfac4  9537  dfac5lem5  9542  dfac2a  9544  dfac2b  9545  dfacacn  9556  dfac12lem3  9560  kmlem2  9566  kmlem13  9577  ackbij1lem16  9646  sornom  9688  infpssrlem4  9717  fin23lem14  9744  fin23lem32  9755  fin23lem34  9757  fin23lem36  9759  isf32lem1  9764  isf32lem2  9765  axcc2lem  9847  axcc3  9849  axcclem  9868  zornn0g  9916  ttukeylem5  9924  ttukeylem6  9925  axrepnd  10005  axpowndlem3  10010  zfcndrep  10025  fpwwe2lem8  10048  pwfseqlem3  10071  wunr1om  10130  wunfi  10132  tskr1om  10178  ingru  10226  grudomon  10228  axgroth3  10242  axgroth4  10243  nqereu  10340  mulcanenq  10371  elnp  10398  elnpi  10399  prlem934  10444  infm3  11589  nnaddcl  11649  nnmulcl  11650  nnne0  11660  peano5uzi  12060  uzind2  12064  nn0indd  12068  zindd  12072  eluzadd  12262  uzaddcl  12293  uzwo  12300  indstr  12305  zmax  12334  xmulasslem  12668  xrsupsslem  12690  xrinfmsslem  12691  xrsupss  12692  xrinfmss  12693  flval2  13174  om2uzlti  13308  uzrdgfni  13316  rabssnn0fi  13344  mptnn0fsupp  13355  seqcl2  13378  seqfveq2  13382  seqshft2  13386  monoord  13390  seqsplit  13393  seqcaopr3  13395  seqf1olem2a  13398  seqf1o  13401  seqid2  13406  seqhomo  13407  ser1const  13416  expcllem  13430  expeq0  13449  mulexp  13458  expadd  13461  expmul  13464  expmordi  13521  leexp2r  13528  leexp1a  13529  bernneq  13580  modexp  13589  facdiv  13637  faclbnd  13640  faclbnd4lem4  13646  hashgadd  13728  hashxp  13785  hashmap  13786  hashf1lem2  13804  hashf1  13805  seqcoll  13812  wrdind  14074  wrd2ind  14075  pfxccatin12lem3  14084  cshweqrep  14173  2cshwcshw  14177  relexp0g  14371  relexpsucnnr  14374  relexpsucnnl  14381  relexpcnv  14384  relexpnndm  14390  relexpaddnn  14400  dfrtrclrec2  14406  rtrclreclem1  14407  rtrclreclem2  14408  rtrclreclem4  14410  dfrtrcl2  14411  relexpind  14413  reusq0  14812  rlim  14842  rlim2  14843  rlim0  14855  rlim0lt  14856  rlimi  14860  ello12r  14864  ello1mpt  14868  ello1d  14870  elo12r  14875  lo1o1  14879  o1lo1  14884  lo1res  14906  climshft  14923  o1compt  14934  rlimo1  14963  lo1add  14973  lo1mul  14974  rlimdiv  14992  climub  15008  climserle  15009  caucvgrlem  15019  caurcvgr  15020  iseraltlem2  15029  summolem2a  15062  sumss  15071  fsum2d  15116  fsumabs  15146  fsumrlim  15156  fsumo1  15157  fsumiun  15166  binom  15175  climcndslem1  15194  climcndslem2  15195  cvgrat  15229  clim2prod  15234  prodfn0  15240  prodfrec  15241  ntrivcvgfvn0  15245  prodmolem2a  15278  fprodabs  15318  fprodn0  15323  fprod2d  15325  binomfallfac  15385  bpolycl  15396  bpolydif  15399  fprodefsum  15438  demoivreALT  15544  ruclem8  15580  ruclem9  15581  dvdsle  15650  dvdsfac  15666  divalglem7  15740  bitsinv1  15781  sadcadd  15797  sadadd2  15799  saddisjlem  15803  smuval2  15821  smupvallem  15822  smu01lem  15824  smupval  15827  smueqlem  15829  smumullem  15831  bezoutlem4  15880  dfgcd2  15884  gcdmultipleOLD  15890  rplpwr  15897  nn0seqcvgd  15904  seq1st  15905  alginv  15909  algcvga  15913  algfx  15914  lcmf  15967  prmind2  16019  prmdvdsexp  16049  prmfac1  16053  reumodprminv  16131  pcmpt  16218  pcfac  16225  prmpwdvds  16230  prmreclem4  16245  vdwlem10  16316  ramval  16334  ramcl  16355  cshwrepswhash1  16426  prmlem1a  16430  imasleval  16804  ismre  16851  mreexexd  16909  lubprop  17586  lublecllem  17588  glbprop  17599  joinlem  17611  meetlem  17625  isglbd  17717  lubun  17723  poslubmo  17746  posglbmo  17747  poslubd  17748  mndind  17982  frmdgsum  18017  mulgnnass  18202  mhmmulg  18208  gsumwrev  18434  gsmsymgrfix  18487  gsmsymgreq  18491  psgnunilem3  18555  sylow1lem1  18654  efginvrel2  18784  efgsrel  18791  efgredlemd  18801  efgredlem  18804  efgred  18805  efgrelexlemb  18807  gsum2dlem2  19022  gsumcom2  19026  ablfac1eulem  19125  pgpfac1lem2  19128  pgpfac1lem5  19132  pgpfac1  19133  pgpfac  19137  srgmulgass  19212  srgpcomp  19213  srgbinom  19226  lmodvsmmulgdi  19600  isdomn2  20002  assamulgscm  20060  mplcoe1  20176  mplcoe3  20177  mplcoe5  20179  gsummoncoe1  20402  cnfldexp  20508  islindf4  20912  dmatval  21031  dmatel  21032  dmatmulcl  21039  pmatcoe1fsupp  21239  decpmataa0  21306  decpmatmulsumfsupp  21311  pmatcollpw2lem  21315  pm2mpmhmlem1  21356  fiinopn  21439  mretopd  21630  neiptoptop  21669  cnpfval  21772  iscnp3  21782  tgcn  21790  lmbr  21796  lmbr2  21797  lmbrf  21798  lmss  21836  ishaus  21860  hausnei2  21891  t1sep2  21907  fiuncmp  21942  dfconn2  21957  1stcfb  21983  2ndc1stc  21989  1stcrest  21991  1stcelcls  21999  1stccn  22001  lly1stc  22034  elkgen  22074  kgencn  22094  tx1stc  22188  xkopt  22193  cnmptcom  22216  isr0  22275  r0sep  22286  ptcmpfi  22351  isfildlem  22395  rnelfm  22491  fbflim  22514  flimrest  22521  isflf  22531  flffbas  22533  lmflf  22543  fclsrest  22562  isfcf  22572  cnextfvval  22603  tmdgsum  22633  eltsms  22670  tsmsi  22671  tsmsgsum  22676  tsmssubm  22680  tsmsres  22681  tsmsf1o  22682  isust  22741  isucn  22816  isucn2  22817  ucnima  22819  imasdsf1olem  22912  metss  23047  met1stc  23060  metcnp  23080  metcnpi  23083  metcnpi2  23084  metucn  23110  xrge0tsms  23371  fsumcn  23407  elcncf  23426  cncfi  23431  rescncf  23434  cncfco  23444  caucfil  23815  equivcau  23832  caubl  23840  caublcls  23841  ovolgelb  24010  ovolunlem1a  24026  ovolicc2lem3  24049  voliunlem1  24080  voliunlem3  24082  volsuplem  24085  volsup  24086  dyadmax  24128  vitali  24143  itg2leub  24264  itgfsum  24356  dvnadd  24455  dvnres  24457  cpnord  24461  dvnfre  24478  dvmptfsum  24501  dvferm1  24511  dvferm2  24513  rolle  24516  dvlip  24519  c1lip1  24523  lhop1  24540  deg1leb  24618  ply1divex  24659  fta1g  24690  plyco  24760  dgrcolem1  24792  dgrco  24794  dvnply2  24805  plydivex  24815  aalioulem2  24851  aalioulem3  24852  aalioulem5  24854  aaliou3lem2  24861  dvntaylp  24888  taylthlem1  24890  ulmdvlem3  24919  abelthlem9  24957  cxpmul2  25199  scvxcvx  25491  jensenlem2  25493  jensen  25494  wilthlem3  25575  perfectlem2  25734  bcmono  25781  bposlem5  25792  lgsquad2lem2  25889  addsq2reu  25944  2sqreulem1  25950  2sqreunnlem1  25953  dchrisumlem1  25993  dchrisum0flb  26014  pntpbnd1  26090  pntlemf  26109  qabvle  26129  qabvexp  26130  ostthlem2  26132  ostth2lem2  26138  tgcgr4  26245  usgr2pth  27473  wlkiswwlks2lem4  27578  wlkiswwlks2  27581  rusgrnumwwlk  27682  clwlkclwwlklem2a  27704  clwlkclwwlklem1  27705  clwlkclwwlkfo  27715  eupth2  27946  frgr3vlem1  27980  3vfriswmgrlem  27984  3vfriswmgr  27985  wlkl0  28074  numclwlk2lem2f1o  28086  isplig  28181  isnvlem  28315  nvi  28319  nmoubi  28477  nmounbi  28481  nmblolbi  28505  ipasslem1  28536  ipassi  28546  hlim2  28897  pjhth  29098  spansni  29262  elspansn2  29272  pjige0  29396  pjcjt2  29397  pjopyth  29425  elcnop  29562  elcnfn  29587  nmopub  29613  cnopc  29618  nmfnleub  29630  elnlfn  29633  cnfnc  29635  nmbdoplb  29730  nmcexi  29731  nmcoplb  29735  lnfnmul  29753  nmbdfnlb  29755  nmcfnlb  29759  pjss2coi  29869  pjssmi  29870  isst  29918  ishst  29919  stcltr1i  29979  mdbr  29999  dmdbr  30004  mddmd2  30014  mdslmd1lem3  30032  mdslmd1lem4  30033  elat2  30045  atcvat2  30094  cdj1i  30138  iuninc  30241  fmptcof2  30331  nnindd  30463  nn0min  30464  wrdt2ind  30555  xrge0tsmsd  30620  isomnd  30630  omndadd  30635  cyc3genpm  30722  isarchi2  30742  archirng  30745  archiexdiv  30747  archiabl  30755  isorng  30800  ofldchr  30815  crefeq  31009  nexple  31168  esumfzf  31228  issiga  31271  isrnsiga  31272  isldsys  31315  ismeas  31358  isrnmeas  31359  measiun  31377  eulerpartlemn  31539  sseqp1  31553  rrvsum  31612  signsply0  31721  signstfvc  31744  bnj941  31944  bnj106  32040  bnj155  32051  bnj590  32082  bnj591  32083  bnj849  32097  bnj893  32100  bnj944  32110  bnj1128  32160  subfacp1lem6  32330  erdszelem8  32343  issconn  32371  cvmliftlem7  32436  cvmliftlem10  32439  cvmlift3lem2  32465  satfsschain  32509  satfrel  32512  satfdm  32514  satfrnmapom  32515  fmlafvel  32530  satffun  32554  mrsubvrs  32667  mclsssvlem  32707  mclsval  32708  mclsax  32714  mclsind  32715  shftvalg  32861  bccolsum  32869  iprodefisumlem  32870  faclimlem1  32873  dfpo2  32889  rdgprc  32937  trpredmintr  32968  frmin  32982  soseq  32994  frr3g  33019  fpr3g  33020  frrlem12  33032  fpr2  33038  frr2  33043  nosupno  33101  nosupdm  33102  nosupfv  33104  nosupres  33105  nosupbnd1lem1  33106  nosupbnd1lem3  33108  nosupbnd1lem5  33110  noeta  33120  fveleq  33697  unblimceq0  33744  bj-ax12  33888  bj-bm1.3ii  34252  rdgeqoa  34534  finxpreclem6  34560  domalom  34568  ralssiun  34571  wl-sblimt  34669  wl-sbhbt  34672  wl-2sb6d  34676  wl-mo2df  34688  wl-mo2t  34693  poimirlem2  34776  poimirlem25  34799  poimirlem28  34802  poimirlem31  34805  heicant  34809  mbfresfi  34820  itg2gt0cn  34829  sdclem2  34900  fdc  34903  seqpo  34905  incsequz  34906  mettrifi  34915  prdsbnd2  34956  heiborlem4  34975  bfplem1  34983  iscringd  35159  maxidlval  35200  igenval2  35227  iss2  35484  elrefrels3  35640  ax12eq  35959  ax12el  35960  ax12indalem  35963  ax12inda2ALT  35964  ax12inda  35966  ax12v2-o  35967  riotasvd  35974  isopos  36198  isat3  36325  ishlat1  36370  glbconN  36395  ispsubsp  36763  isldil  37128  isltrn  37137  isdilN  37172  trlval  37180  cdleme27b  37386  cdleme29b  37393  cdleme31sn1  37399  cdleme31sn1c  37406  cdleme40v  37487  cdlemk36  37931  cdlemkid5  37953  cdlemn11pre  38228  dihord2pre  38243  islpolN  38501  hdmapffval  38844  hdmapfval  38845  hdmapval2lem  38849  nnaddcom  39041  nnadddir  39043  nnmulcom  39045  ismrc  39178  incssnn0  39188  mzpexpmpt  39222  pell14qrexpclnn0  39343  monotuz  39418  rmxypos  39424  jm2.17a  39437  jm2.17b  39438  rmygeid  39441  jm2.18  39465  jm2.19lem3  39468  jm2.25  39476  jm2.15nn0  39480  jm2.16nn0  39481  wepwsolem  39522  aomclem8  39541  dfac11  39542  pwslnm  39574  lnr2i  39596  hbtlem5  39608  cnsrexpcl  39645  rngunsnply  39653  isdomn3  39684  ifpbi23  39718  elmapintrab  39816  elmapintab  39836  cnvcnvintabd  39840  eliunov2  39904  relexpxpnnidm  39928  relexpiidm  39929  relexpss1d  39930  iunrelexpmin1  39933  relexpmulnn  39934  iunrelexpmin2  39937  relexp0a  39941  trclimalb2  39951  clsk3nimkb  40270  ntrclsiso  40297  ntrclskb  40299  ntrneiiso  40321  ntrneix2  40323  ntrneixb  40325  gneispace2  40362  gneispacess2  40376  mnuunid  40493  dvgrat  40524  pm14.122b  40635  fnchoice  41166  fiiuncl  41207  ssinc  41233  ssdec  41234  wessf1ornlem  41325  dmrelrnrel  41370  fperiodmullem  41450  monoordxrv  41638  fmul01  41741  fmuldfeq  41744  climsuselem1  41768  climinff  41772  ellimcabssub0  41778  limcleqr  41805  addlimc  41809  0ellimcdiv  41810  limclner  41812  limsupref  41846  limsupub  41865  limsupmnf  41882  limsupre2lem  41885  limsupre2  41886  limsupre2mpt  41891  limsupre3lem  41893  limsupre3  41894  limsupre3mpt  41895  xlimbr  41988  cnrefiisplem  41990  dvnmptdivc  42103  dvnmptconst  42106  dvnmul  42108  iblspltprt  42138  itgspltprt  42144  stoweidlem2  42168  stoweidlem3  42169  stoweidlem17  42183  stoweidlem19  42185  stoweidlem21  42187  stoweidlem26  42192  fourierdlem42  42315  issal  42480  ismea  42614  isome  42657  carageniuncllem1  42684  caratheodorylem1  42689  2reu8i  43193  2reuimp0  43194  funressndmafv2rn  43303  2ffzoeq  43409  smonoord  43412  fargshiftf1  43448  paireqne  43520  reupr  43531  reuopreuprim  43535  perfectALTVlem2  43734  lmodvsmdi  44328  dmatALTval  44353  dmatALTbasel  44355  snlindsntor  44424  ldepsnlinc  44461  elbigo2r  44511  elbigolo1  44515  setrecseq  44686  setrec2fun  44693  setrec2lem2  44695
  Copyright terms: Public domain W3C validator