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

Theorem imbi2d 330
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  334  imbi2  338  pm5.42  570  orbi2d  737  con3ALT  1031  con3OLD  1034  axc15  2302  ax12v2OLD  2341  axc14  2371  mo2  2478  2gencl  3226  3gencl  3227  vtocl2gf  3258  vtocl3gf  3259  vtocl4g  3267  eqeu  3364  mo2icl  3372  euind  3380  reu7  3388  reuind  3398  sbctt  3487  sbcnestgf  3973  r19.36zv  4050  dedth2h  4118  dedth3h  4119  dedth4h  4120  preq12bg  4361  prel12g  4362  elint  4453  elintrabg  4461  intab  4479  trssOLD  4732  axrep1  4742  axrep2  4743  axrep3  4744  bm1.3ii  4754  reusv3  4846  pocl  5012  swopolem  5014  solin  5028  freq1  5054  frminex  5064  vtoclr  5134  2optocl  5167  3optocl  5168  raliunxp  5231  resieq  5376  iss  5416  cnveqb  5559  preddowncl  5676  funmo  5873  funimaexg  5943  fnbrfvb  6203  fvelimab  6220  fvmptss  6259  fmptco  6362  fprg  6387  fnressn  6390  fressnfv  6392  isoselem  6556  ovg  6764  caovcan  6803  caovordig  6804  caovord  6810  tfisi  7020  tfindsg  7022  tfinds2  7025  tfinds3  7026  dfom2  7029  elom  7030  findsg  7055  finds2  7056  f1o2ndf1  7245  poxp  7249  fnse  7254  wfr3g  7373  wfrlem4  7378  smoeq  7407  smores  7409  smogt  7424  tfrlem1  7432  tfr3  7455  oaordi  7586  oeordi  7627  oeoa  7637  oeoe  7639  nnacl  7651  nnmcl  7652  nnecl  7653  nnacom  7657  nnaordi  7658  nnawordi  7661  nnaass  7662  nndi  7663  nnmass  7664  nnmsucr  7665  nnmcom  7666  nnmordi  7671  2ecoptocl  7798  3ecoptocl  7799  undifixp  7904  xpdom2g  8016  findcard2  8160  xpfi  8191  fnfi  8198  fodomfi  8199  finsschain  8233  marypha1lem  8299  marypha1  8300  supeq1  8311  ordiso2  8380  ordtypelem7  8389  wemaplem1  8411  inf3lem2  8486  inf3lem5  8489  infdiffi  8515  cantnfval2  8526  cantnfle  8528  cantnfp1lem3  8537  oemapval  8540  cantnflem1  8546  cantnf  8550  wemapwe  8554  cnfcom  8557  cnfcom3clem  8562  tz9.1  8565  r1pwALT  8669  cplem2  8713  karden  8718  infxpenc2lem2  8803  fseqenlem1  8807  dfac8clem  8815  alephinit  8878  dfac4  8905  dfac5lem5  8910  dfac2a  8912  dfac2  8913  dfacacn  8923  dfac12lem3  8927  kmlem2  8933  kmlem13  8944  ackbij1lem16  9017  sornom  9059  infpssrlem4  9088  fin23lem14  9115  fin23lem32  9126  fin23lem34  9128  fin23lem36  9130  isf32lem1  9135  isf32lem2  9136  axcc2lem  9218  axcc3  9220  axcclem  9239  zornn0g  9287  ttukeylem5  9295  ttukeylem6  9296  axrepnd  9376  axpowndlem3  9381  zfcndrep  9396  fpwwe2lem8  9419  pwfseqlem3  9442  wunr1om  9501  wunfi  9503  tskr1om  9549  ingru  9597  grudomon  9599  axgroth3  9613  axgroth4  9614  nqereu  9711  mulcanenq  9742  elnp  9769  elnpi  9770  prlem934  9815  infm3  10942  nnaddcl  11002  nnmulcl  11003  peano5uzi  11426  uzind2  11430  nn0indd  11434  zindd  11438  eluzadd  11676  uzaddcl  11704  uzwo  11711  indstr  11716  zmax  11745  xmulasslem  12074  xrsupsslem  12096  xrinfmsslem  12097  xrsupss  12098  xrinfmss  12099  flval2  12571  om2uzlti  12705  uzrdgfni  12713  rabssnn0fi  12741  mptnn0fsupp  12753  seqcl2  12775  seqfveq2  12779  seqshft2  12783  monoord  12787  seqsplit  12790  seqcaopr3  12792  seqf1olem2a  12795  seqf1o  12798  seqid2  12803  seqhomo  12804  ser1const  12813  expcllem  12827  expeq0  12846  mulexp  12855  expadd  12858  expmul  12861  leexp2r  12874  leexp1a  12875  bernneq  12946  modexp  12955  facdiv  13030  faclbnd  13033  faclbnd4lem4  13039  faclbnd6  13042  hashgadd  13122  hashxp  13177  hashmap  13178  hashf1lem2  13194  hashf1  13195  seqcoll  13202  wrdind  13430  wrd2ind  13431  swrdccatin12lem3  13443  cshweqrep  13520  2cshwcshw  13524  relexp0g  13712  relexpsucnnr  13715  relexpsucnnl  13722  relexpcnv  13725  relexpnndm  13731  relexpaddnn  13741  dfrtrclrec2  13747  rtrclreclem1  13748  rtrclreclem2  13749  rtrclreclem4  13751  dfrtrcl2  13752  relexpind  13754  cjexp  13840  absexp  13994  rlim  14176  rlim2  14177  rlim0  14189  rlim0lt  14190  rlimi  14194  ello12r  14198  ello1mpt  14202  ello1d  14204  elo12r  14209  lo1o1  14213  o1lo1  14218  lo1res  14240  climshft  14257  o1compt  14268  rlimo1  14297  lo1add  14307  lo1mul  14308  rlimdiv  14326  climub  14342  climserle  14343  caucvgrlem  14353  caurcvgr  14354  iseraltlem2  14363  summolem2a  14395  sumss  14404  fsum2d  14449  fsumabs  14479  fsumrlim  14489  fsumo1  14490  fsumiun  14499  binom  14506  bcxmas  14511  climcndslem1  14525  climcndslem2  14526  cvgrat  14559  clim2prod  14564  prodfn0  14570  prodfrec  14571  ntrivcvgfvn0  14575  prodmolem2a  14608  fprodabs  14648  fprodn0  14653  fprod2d  14655  binomfallfac  14716  bpolycl  14727  bpolydif  14730  fprodefsum  14769  demoivreALT  14875  ruclem8  14910  ruclem9  14911  dvdsle  14975  dvdsfac  14991  divalglem7  15065  bitsinv1  15107  sadcadd  15123  sadadd2  15125  saddisjlem  15129  smuval2  15147  smupvallem  15148  smu01lem  15150  smupval  15153  smueqlem  15155  smumullem  15157  bezoutlem4  15202  dfgcd2  15206  gcdmultiple  15212  rplpwr  15219  nn0seqcvgd  15226  seq1st  15227  alginv  15231  algcvga  15235  algfx  15236  lcmf  15289  prmind2  15341  prmdvdsexp  15370  prmfac1  15374  reumodprminv  15452  pcmpt  15539  pcfac  15546  prmpwdvds  15551  prmreclem4  15566  vdwlem10  15637  ramval  15655  ramcl  15676  cshwrepswhash1  15752  prmlem1a  15756  imasleval  16141  ismre  16190  mreexexd  16248  mreexexdOLD  16249  lubprop  16926  lublecllem  16928  glbprop  16939  joinlem  16951  meetlem  16965  isglbd  17057  lubun  17063  poslubmo  17086  posglbmo  17087  poslubd  17088  mrcmndind  17306  frmdgsum  17339  mulgnnass  17516  mulgnnassOLD  17517  mhmmulg  17523  gsumwrev  17736  gsmsymgrfix  17788  gsmsymgreq  17792  psgnunilem3  17856  sylow1lem1  17953  efginvrel2  18080  efgsrel  18087  efgredlemd  18097  efgredlem  18100  efgred  18101  efgrelexlemb  18103  gsum2dlem2  18310  gsumcom2  18314  ablfac1eulem  18411  pgpfac1lem2  18414  pgpfac1lem5  18418  pgpfac1  18419  pgpfac  18423  srgmulgass  18471  srgpcomp  18472  srgbinom  18485  lmodvsmmulgdi  18838  isdomn2  19239  assamulgscm  19290  mplcoe1  19405  mplcoe3  19406  mplcoe5  19408  gsummoncoe1  19614  cnfldexp  19719  islindf4  20117  dmatval  20238  dmatel  20239  dmatmulcl  20246  pmatcoe1fsupp  20446  decpmataa0  20513  decpmatmulsumfsupp  20518  pmatcollpw2lem  20522  pm2mpmhmlem1  20563  fiinopn  20646  mretopd  20836  neiptoptop  20875  cnpfval  20978  iscnp3  20988  tgcn  20996  lmbr  21002  lmbr2  21003  lmbrf  21004  lmss  21042  ishaus  21066  hausnei2  21097  t1sep2  21113  fiuncmp  21147  dfconn2  21162  1stcfb  21188  2ndc1stc  21194  1stcrest  21196  1stcelcls  21204  1stccn  21206  lly1stc  21239  elkgen  21279  kgencn  21299  tx1stc  21393  xkopt  21398  cnmptcom  21421  isr0  21480  r0sep  21491  ptcmpfi  21556  isfildlem  21601  rnelfm  21697  fbflim  21720  flimrest  21727  isflf  21737  flffbas  21739  lmflf  21749  fclsrest  21768  isfcf  21778  cnextfvval  21809  tmdmulg  21836  tmdgsum  21839  eltsms  21876  tsmsi  21877  tsmsgsum  21882  tsmssubm  21886  tsmsres  21887  tsmsf1o  21888  isust  21947  isucn  22022  isucn2  22023  ucnima  22025  imasdsf1olem  22118  metss  22253  met1stc  22266  metcnp  22286  metcnpi  22289  metcnpi2  22290  metucn  22316  xrge0tsms  22577  fsumcn  22613  elcncf  22632  cncfi  22637  rescncf  22640  cncfco  22650  caucfil  23021  equivcau  23038  caubl  23046  caublcls  23047  ovolgelb  23188  ovolunlem1a  23204  ovolicc2lem3  23227  voliunlem1  23258  voliunlem3  23260  volsuplem  23263  volsup  23264  dyadmax  23306  vitali  23322  itg2leub  23441  itgfsum  23533  dvnadd  23632  dvnres  23634  cpnord  23638  dvnfre  23655  dvmptfsum  23676  dvferm1  23686  dvferm2  23688  rolle  23691  dvlip  23694  c1lip1  23698  lhop1  23715  deg1leb  23793  ply1divex  23834  fta1g  23865  plyco  23935  dgrcolem1  23967  dgrco  23969  dvnply2  23980  plydivex  23990  aalioulem2  24026  aalioulem3  24027  aalioulem5  24029  aaliou3lem2  24036  dvntaylp  24063  taylthlem1  24065  ulmdvlem3  24094  abelthlem9  24132  cxpmul2  24369  scvxcvx  24646  jensenlem2  24648  jensen  24649  wilthlem3  24730  perfectlem2  24889  bcmono  24936  bposlem5  24947  lgsquad2lem2  25044  dchrisumlem1  25112  dchrisum0flb  25133  pntpbnd1  25209  pntlemf  25228  qabvle  25248  qabvexp  25249  ostthlem2  25251  ostth2lem2  25257  tgcgr4  25360  usgr2pth  26563  wlkiswwlks2lem4  26661  wlkiswwlks2  26664  rusgrnumwwlk  26771  clwlkclwwlklem2a  26800  clwlkclwwlklem1  26801  clwlksfoclwwlk  26863  eupth2  26999  frgr3vlem1  27035  3vfriswmgrlem  27039  3vfriswmgr  27040  numclwlk2lem2f1o  27127  isplig  27216  isnvlem  27353  nvi  27357  nmoubi  27515  nmounbi  27519  nmblolbi  27543  ipasslem1  27574  ipassi  27584  hlim2  27937  pjhth  28140  spansni  28304  elspansn2  28314  pjige0  28438  pjcjt2  28439  pjopyth  28467  elcnop  28604  elcnfn  28629  nmopub  28655  cnopc  28660  nmfnleub  28672  elnlfn  28675  cnfnc  28677  nmbdoplb  28772  nmcexi  28773  nmcoplb  28777  lnfnmul  28795  nmbdfnlb  28797  nmcfnlb  28801  pjss2coi  28911  pjssmi  28912  isst  28960  ishst  28961  stcltr1i  29021  mdbr  29041  dmdbr  29046  mddmd2  29056  mdslmd1lem3  29074  mdslmd1lem4  29075  elat2  29087  atcvat2  29136  cdj1i  29180  vtocl2d  29203  rmoeqALT  29216  iuninc  29265  fmptcof2  29340  nnindd  29449  nn0min  29450  isomnd  29528  omndadd  29533  isarchi2  29566  archirng  29569  archiexdiv  29571  archiabl  29579  xrge0tsmsd  29612  isorng  29626  ofldchr  29641  crefeq  29736  nexple  29895  esumfzf  29954  issiga  29997  isrnsiga  29999  isldsys  30042  ismeas  30085  isrnmeas  30086  measiun  30104  eulerpartlemn  30266  sseqp1  30280  rrvsum  30339  signsply0  30450  signstfvc  30473  bnj941  30604  bnj106  30699  bnj155  30710  bnj590  30741  bnj591  30742  bnj849  30756  bnj893  30759  bnj944  30769  bnj1128  30819  subfacp1lem6  30928  erdszelem8  30941  issconn  30969  cvmliftlem7  31034  cvmliftlem10  31037  cvmlift3lem2  31063  mrsubvrs  31180  mclsssvlem  31220  mclsval  31221  mclsax  31227  mclsind  31228  shftvalg  31378  bccolsum  31386  iprodefisumlem  31387  faclimlem1  31390  dfpo2  31406  br1steqg  31429  br2ndeqg  31430  rdgprc  31454  trpredmintr  31485  frmin  31493  soseq  31505  frr3g  31533  nosino  31628  nosifv  31629  nosires  31630  fveleq  32145  unblimceq0  32193  bj-axrep1  32484  bj-axrep2  32485  bj-axrep3  32486  rdgeqoa  32889  finxpreclem6  32904  wl-sblimt  33003  wl-sbhbt  33006  wl-2sb6d  33012  wl-mo2df  33023  wl-mo2t  33028  poimirlem2  33082  poimirlem25  33105  poimirlem28  33108  poimirlem31  33111  heicant  33115  mbfresfi  33127  itg2gt0cn  33136  sdclem2  33209  fdc  33212  seqpo  33214  incsequz  33215  mettrifi  33224  prdsbnd2  33265  heiborlem4  33284  bfplem1  33292  iscringd  33468  maxidlval  33509  igenval2  33536  ax12eq  33745  ax12el  33746  ax12indalem  33749  ax12inda2ALT  33750  ax12inda  33752  ax12v2-o  33753  riotasvd  33761  isopos  33986  isat3  34113  ishlat1  34158  glbconN  34182  ispsubsp  34550  isldil  34915  isltrn  34924  isdilN  34960  trlval  34968  cdleme27b  35175  cdleme29b  35182  cdleme31sn1  35188  cdleme31sn1c  35195  cdleme40v  35276  cdlemk36  35720  cdlemkid5  35742  cdlemn11pre  36018  dihord2pre  36033  islpolN  36291  hdmapffval  36637  hdmapfval  36638  hdmapval2lem  36642  ismrc  36783  incssnn0  36793  mzpexpmpt  36827  pell14qrexpclnn0  36949  monotuz  37025  expmordi  37031  rmxypos  37033  jm2.17a  37046  jm2.17b  37047  rmygeid  37050  jm2.18  37074  jm2.19lem3  37077  jm2.25  37085  jm2.15nn0  37089  jm2.16nn0  37090  wepwsolem  37131  aomclem8  37150  dfac11  37151  pwslnm  37183  lnr2i  37206  hbtlem5  37218  cnsrexpcl  37255  rngunsnply  37263  isdomn3  37302  ifpbi23  37337  elmapintrab  37402  elmapintab  37422  cnvcnvintabd  37426  eliunov2  37491  relexpxpnnidm  37515  relexpiidm  37516  relexpss1d  37517  iunrelexpmin1  37520  relexpmulnn  37521  iunrelexpmin2  37524  relexp0a  37528  trclimalb2  37538  clsk3nimkb  37859  ntrclsiso  37886  ntrclskb  37888  ntrneiiso  37910  ntrneix2  37912  ntrneixb  37914  gneispace2  37951  gneispacess2  37965  dvgrat  38032  pm14.122b  38145  fnchoice  38710  fiiuncl  38756  ssinc  38786  ssdec  38787  wessf1ornlem  38880  dmrelrnrel  38928  fperiodmullem  39016  fmul01  39248  fmuldfeq  39251  climsuselem1  39275  climinff  39279  ellimcabssub0  39285  limcleqr  39312  addlimc  39316  0ellimcdiv  39317  limclner  39319  limsupref  39353  limsupub  39372  limsupmnf  39389  limsupre2lem  39392  limsupre2  39393  limsupre2mpt  39398  limsupre3lem  39400  limsupre3  39401  limsupre3mpt  39402  dvnmptdivc  39490  dvnmptconst  39493  dvnmul  39495  iblspltprt  39526  itgspltprt  39532  stoweidlem2  39556  stoweidlem3  39557  stoweidlem17  39571  stoweidlem19  39573  stoweidlem21  39575  stoweidlem26  39580  fourierdlem42  39703  issal  39871  ismea  40005  isome  40045  carageniuncllem1  40072  caratheodorylem1  40077  2ffzoeq  40665  smonoord  40669  fargshiftf1  40705  perfectALTVlem2  40956  lmodvsmdi  41481  dmatALTval  41507  dmatALTbasel  41509  snlindsntor  41578  ldepsnlinc  41615  elbigo2r  41669  elbigolo1  41673  setrecseq  41755  setrec2fun  41762  setrec2lem2  41764
  Copyright terms: Public domain W3C validator