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

Theorem imbi2d 307
Description: Deduction adding an antecedent to both sides of a logical equivalence. (Contributed by NM, 5-Aug-1993.)
Hypothesis
Ref Expression
imbid.1  |-  ( ph  ->  ( ps  <->  ch )
)
Assertion
Ref Expression
imbi2d  |-  ( ph  ->  ( ( th  ->  ps )  <->  ( th  ->  ch ) ) )

Proof of Theorem imbi2d
StepHypRef Expression
1 imbid.1 . . 3  |-  ( ph  ->  ( ps  <->  ch )
)
21a1d 22 . 2  |-  ( ph  ->  ( th  ->  ( ps 
<->  ch ) ) )
32pm5.74d 238 1  |-  ( ph  ->  ( ( th  ->  ps )  <->  ( th  ->  ch ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176
This theorem is referenced by:  imbi12d  311  imbi2  314  pm5.42  531  orbi2d  682  con3th  924  19.23t  1796  ax12olem6  1873  ax11v2  1932  ax15  1961  nfsb4t  2020  sbcom  2029  sbcom2  2053  ax11eq  2132  ax11el  2133  ax11indalem  2136  ax11inda2ALT  2137  ax11inda  2139  ax11v2-o  2140  mo  2165  2mo  2221  2eu6  2228  2gencl  2817  3gencl  2818  vtocl2gf  2845  vtocl3gf  2846  eqeu  2936  mo2icl  2944  euind  2952  reu7  2960  reuind  2968  sbctt  3053  sbcnestgf  3128  r19.36zv  3554  dedth2h  3607  dedth3h  3608  dedth4h  3609  preq12bg  3791  elint  3868  elintrabg  3875  intab  3892  trss  4122  axrep1  4132  axrep2  4133  axrep3  4134  bm1.3ii  4144  pocl  4321  swopolem  4323  solin  4337  freq1  4363  frminex  4373  reusv3  4542  tfisi  4649  tfindsg  4651  tfinds2  4654  tfinds3  4655  dfom2  4658  elom  4659  findsg  4683  finds2  4684  vtoclr  4733  2optocl  4765  3optocl  4766  raliunxp  4825  resieq  4965  iss  4998  cnveqb  5129  funmo  5271  funimaexg  5329  fnbrfvb  5563  fvelimab  5578  fvmptss  5609  fmptco  5691  fnressn  5705  fressnfv  5707  f1fveq  5786  isoselem  5838  ovg  5986  caovcan  6024  caovordig  6025  caovord  6031  poxp  6227  fnse  6232  riotasvd  6347  riotasvdOLD  6348  smoeq  6367  smores  6369  smogt  6384  tfrlem1  6391  tfr3  6415  oaordi  6544  oeordi  6585  oeoa  6595  oeoe  6597  nnacl  6609  nnmcl  6610  nnecl  6611  nnacom  6615  nnaordi  6616  nnawordi  6619  nnaass  6620  nndi  6621  nnmass  6622  nnmsucr  6623  nnmcom  6624  nnmordi  6629  2ecoptocl  6749  3ecoptocl  6750  th3qlem2  6765  undifixp  6852  xpdom2g  6958  findcard2  7098  xpfi  7128  fnfi  7134  fodomfi  7135  finsschain  7162  marypha1lem  7186  marypha1  7187  supeq1  7198  ordiso2  7230  ordtypelem7  7239  wemaplem1  7261  inf3lem2  7330  inf3lem5  7333  infdiffi  7358  cantnfval2  7370  cantnfle  7372  cantnfp1lem3  7382  oemapval  7385  cantnflem1  7391  cantnf  7395  wemapwe  7400  cnfcom  7403  cnfcom3clem  7408  tz9.1  7411  r1pwOLD  7518  cplem2  7560  karden  7565  infxpenc2lem2  7647  fseqenlem1  7651  dfac8clem  7659  alephinit  7722  dfac4  7749  dfac5lem5  7754  dfac2a  7756  dfac2  7757  dfacacn  7767  dfac12lem3  7771  kmlem2  7777  kmlem13  7788  ackbij1lem16  7861  sornom  7903  infpssrlem4  7932  fin23lem14  7959  fin23lem32  7970  fin23lem34  7972  fin23lem36  7974  isf32lem1  7979  isf32lem2  7980  axcc2lem  8062  axcc3  8064  axcclem  8083  zornn0g  8132  ttukeylem5  8140  ttukeylem6  8141  axrepnd  8216  axpowndlem3  8221  zfcndrep  8236  fpwwe2lem8  8259  pwfseqlem3  8282  wunr1om  8341  wunfi  8343  tskr1om  8389  ingru  8437  grudomon  8439  axgroth3  8453  axgroth4  8454  nqereu  8553  mulcanenq  8584  elnp  8611  elnpi  8612  prlem934  8657  infm3  9713  nnaddcl  9768  nnmulcl  9769  peano5uzi  10100  uzind2  10104  uzindOLD  10106  zindd  10113  eluzadd  10256  uzaddcl  10275  uzwo  10281  uzwoOLD  10282  indstr  10287  zmax  10313  xmulasslem  10605  xrsupsslem  10625  xrinfmsslem  10626  xrsupss  10627  xrinfmss  10628  flval2  10944  om2uzlti  11013  uzrdgfni  11021  seqcl2  11064  seqfveq2  11068  seqshft2  11072  monoord  11076  seqsplit  11079  seqcaopr3  11081  seqf1olem2a  11084  seqf1o  11087  seqid2  11092  seqhomo  11093  ser1const  11102  expcllem  11114  expeq0  11132  mulexp  11141  expadd  11144  expmul  11147  leexp2r  11159  leexp1a  11160  bernneq  11227  modexp  11236  facdiv  11300  faclbnd  11303  faclbnd4lem4  11309  faclbnd6  11312  hashgadd  11359  hashxp  11386  hashmap  11387  hashf1lem2  11394  hashf1  11395  seqcoll  11401  wrdind  11477  cjexp  11635  absexp  11789  rlim  11969  rlim2  11970  rlim0  11982  rlim0lt  11983  rlimi  11987  ello12r  11991  ello1mpt  11995  ello1d  11997  elo12r  12002  lo1o1  12006  o1lo1  12011  lo1res  12033  climshft  12050  o1compt  12061  rlimo1  12090  lo1add  12100  lo1mul  12101  rlimdiv  12119  climub  12135  climserle  12136  caucvgrlem  12145  caurcvgr  12146  iseraltlem2  12155  summolem2a  12188  sumss  12197  fsum2d  12234  fsumabs  12259  fsumrlim  12269  fsumo1  12270  fsumiun  12279  binom  12288  bcxmas  12294  climcndslem1  12308  climcndslem2  12309  cvgrat  12339  demoivreALT  12481  ruclem8  12515  ruclem9  12516  dvdsle  12574  dvdsfac  12583  divalglem7  12598  bitsinv1  12633  sadcadd  12649  sadadd2  12651  saddisjlem  12655  smuval2  12673  smupvallem  12674  smu01lem  12676  smupval  12679  smueqlem  12681  smumullem  12683  bezoutlem4  12720  gcdmultiple  12729  rplpwr  12735  nn0seqcvgd  12740  seq1st  12741  alginv  12745  algcvga  12749  algfx  12750  prmind2  12769  prmdvdsexp  12793  prmfac1  12797  pcmpt  12940  pcfac  12947  prmpwdvds  12951  prmreclem4  12966  vdwlem10  13037  ramval  13055  ramcl  13076  prmlem1a  13108  imasleval  13443  ismre  13492  mreexexd  13550  lubprop  14114  lubid  14116  glbprop  14119  joinlem  14124  meetlem  14131  isglbd  14221  lubun  14227  oduclatb  14248  poslubmo  14250  poslubd  14251  spwmo  14335  spwpr4  14340  frmdgsum  14484  mulgnnass  14595  mhmmulg  14599  gsumwrev  14839  sylow1lem1  14909  efginvrel2  15036  efgsrel  15043  efgredlemd  15053  efgredlem  15056  efgred  15057  efgrelexlemb  15059  gsum2d  15223  gsumcom2  15226  ablfac1eulem  15307  pgpfac1lem2  15310  pgpfac1lem5  15314  pgpfac1  15315  pgpfac  15319  isdomn2  16040  mplcoe1  16209  mplcoe3  16210  mplcoe2  16211  cnfldexp  16407  fiinopn  16647  mretopd  16829  cnpfval  16964  iscnp3  16974  tgcn  16982  lmbr  16988  lmbr2  16989  lmbrf  16990  lmss  17026  ishaus  17050  hausnei2  17081  t1sep2  17097  fiuncmp  17131  dfcon2  17145  1stcfb  17171  2ndc1stc  17177  1stcrest  17179  1stcelcls  17187  1stccn  17189  lly1stc  17222  elkgen  17231  kgencn  17251  tx1stc  17344  xkopt  17349  cnmptcom  17372  isr0  17428  r0sep  17439  ptcmpfi  17504  isfildlem  17552  rnelfm  17648  fbflim  17671  flimrest  17678  isflf  17688  flffbas  17690  lmflf  17700  fclsrest  17719  isfcf  17729  tmdmulg  17775  tmdgsum  17778  eltsms  17815  tsmsi  17816  tsmsgsum  17821  tsmssubm  17825  tsmsres  17826  tsmsf1o  17827  imasdsf1olem  17937  metss  18054  met1stc  18067  metcnp  18087  metcnpi  18090  metcnpi2  18091  xrge0tsms  18339  fsumcn  18374  elcncf  18393  cncfi  18398  rescncf  18401  cncfco  18411  caucfil  18709  equivcau  18726  caubl  18733  caublcls  18734  ovolgelb  18839  ovolunlem1a  18855  ovolicc2lem3  18878  voliunlem1  18907  voliunlem3  18909  volsuplem  18912  volsup  18913  dyadmax  18953  vitali  18968  itg2leub  19089  itgfsum  19181  dvnadd  19278  dvnres  19280  cpnord  19284  dvnfre  19301  dvmptfsum  19322  dvferm1  19332  dvferm2  19334  rolle  19337  dvlip  19340  c1lip1  19344  lhop1  19361  deg1leb  19481  ply1divex  19522  fta1g  19553  plyco  19623  dgrcolem1  19654  dgrco  19656  dvnply2  19667  plydivex  19677  aalioulem2  19713  aalioulem3  19714  aalioulem5  19716  aaliou3lem2  19723  dvntaylp  19750  taylthlem1  19752  ulmdvlem3  19779  abelthlem9  19816  cxpmul2  20036  scvxcvx  20280  jensenlem2  20282  jensen  20283  wilthlem3  20308  perfectlem2  20469  bcmono  20516  bposlem5  20527  lgsquad2lem2  20598  dchrisumlem1  20638  dchrisum0flb  20659  pntpbnd1  20735  pntlemf  20754  qabvle  20774  qabvexp  20775  ostthlem2  20777  ostth2lem2  20783  isplig  20844  gxnn0add  20941  gxnn0mul  20944  ghgrp  21035  ghablo  21036  isnvlem  21166  nvi  21170  nmoubi  21350  nmounbi  21354  nmblolbi  21378  ipasslem1  21409  ipassi  21419  hlim2  21771  pjhth  21972  spansni  22136  elspansn2  22146  pjige0  22270  pjcjt2  22271  pjopyth  22299  elcnop  22437  elcnfn  22462  nmopub  22488  cnopc  22493  nmfnleub  22505  elnlfn  22508  cnfnc  22510  nmbdoplb  22605  nmcexi  22606  nmcoplb  22610  lnfnmul  22628  nmbdfnlb  22630  nmcfnlb  22634  pjss2coi  22744  pjssmi  22745  isst  22793  ishst  22794  stcltr1i  22854  mdbr  22874  dmdbr  22879  mddmd2  22889  mdslmd1lem3  22907  mdslmd1lem4  22908  elat2  22920  atcvat2  22969  cdj1i  23013  iuninc  23158  fmptcof2  23229  xrge0iifiso  23317  xrge0tsmsd  23382  issiga  23472  isrnsiga  23474  ismeas  23530  isrnmeas  23531  measiun  23545  subfacp1lem6  23716  erdszelem8  23729  isscon  23757  cvmliftlem7  23822  cvmliftlem10  23825  cvmlift3lem2  23851  eupath2  23904  ghomf1olem  24001  relexp0  24025  relexpsucr  24026  relexpsucl  24028  relexpind  24037  dfrtrclrec2  24040  rtrclreclem.refl  24041  rtrclreclem.subset  24042  rtrclreclem.min  24044  dfrtrcl2  24045  dfpo2  24112  rdgprc  24151  preddowncl  24196  trpredmintr  24234  frmin  24242  soseq  24254  wfr3g  24255  wfrlem4  24259  frr3g  24280  bpolycl  24787  bpolydif  24790  fveleq  24890  elintabg  25090  fprg  25133  cbcpcp  25162  prl2  25169  supdef  25262  inposet  25278  rltrran  25414  svs3  25488  lvsovso  25626  addcanri  25666  issubcv  25670  isded  25736  dedi  25737  iscatOLD  25754  cati  25755  isfunb  25835  fnctartar  25907  fnctartar2  25908  prismorcset2  25918  cmpmor  25975  setiscat  25979  isnword  25986  indcls2  25996  clscnc  26010  pgapspf2  26053  bisig0  26062  isibg2  26110  segline  26141  bsstrs  26146  pdiveql  26168  isibcg  26191  sdclem2  26452  fdc  26455  seqpo  26457  incsequz  26458  mettrifi  26473  prdsbnd2  26519  heiborlem4  26538  bfplem1  26546  iscringd  26624  maxidlval  26664  igenval2  26691  ismrc  26776  incssnn0  26786  mzpexpmpt  26823  pell14qrexpclnn0  26951  monotuz  27026  expmordi  27032  rmxypos  27034  jm2.17a  27047  jm2.17b  27048  rmygeid  27051  divalgmodcl  27080  jm2.18  27081  jm2.19lem3  27084  jm2.25  27092  jm2.15nn0  27096  jm2.16nn0  27097  wepwsolem  27138  aomclem8  27159  dfac11  27160  pwslnm  27196  islindf4  27308  lnr2i  27320  hbtlem5  27332  cnsrexpcl  27370  rngunsnply  27378  psgnunilem3  27419  isdomn3  27523  pm14.122b  27623  fnchoice  27700  fmul01  27710  fmuldfeq  27713  climsuselem1  27733  climinff  27737  stoweidlem2  27751  stoweidlem3  27752  stoweidlem17  27766  stoweidlem21  27770  stoweidlem26  27775  nbusgra  28143  frgra3vlem1  28178  3vfriswmgralem  28182  bnj941  28804  bnj106  28900  bnj155  28911  bnj590  28942  bnj591  28943  bnj849  28957  bnj893  28960  bnj944  28970  bnj1128  29020  a12study2  29134  lubunNEW  29163  isopos  29370  isat3  29497  ishlat1  29542  glbconN  29566  ispsubsp  29934  isldil  30299  isltrn  30308  isdilN  30343  trlval  30351  cdleme27b  30557  cdleme29b  30564  cdleme31sn1  30570  cdleme31sn1c  30577  cdleme40v  30658  cdlemk36  31102  cdlemkid5  31124  cdlemn11pre  31400  dihord2pre  31415  islpolN  31673  hdmapffval  32019  hdmapfval  32020  hdmapval2lem  32024
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177
  Copyright terms: Public domain W3C validator