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

Theorem imbi12d 312
Description: Deduction joining two equivalences to form equivalence of implications. (Contributed by NM, 5-Aug-1993.)
Hypotheses
Ref Expression
imbi12d.1  |-  ( ph  ->  ( ps  <->  ch )
)
imbi12d.2  |-  ( ph  ->  ( th  <->  ta )
)
Assertion
Ref Expression
imbi12d  |-  ( ph  ->  ( ( ps  ->  th )  <->  ( ch  ->  ta ) ) )

Proof of Theorem imbi12d
StepHypRef Expression
1 imbi12d.1 . . 3  |-  ( ph  ->  ( ps  <->  ch )
)
21imbi1d 309 . 2  |-  ( ph  ->  ( ( ps  ->  th )  <->  ( ch  ->  th ) ) )
3 imbi12d.2 . . 3  |-  ( ph  ->  ( th  <->  ta )
)
43imbi2d 308 . 2  |-  ( ph  ->  ( ( ch  ->  th )  <->  ( ch  ->  ta ) ) )
52, 4bitrd 245 1  |-  ( ph  ->  ( ( ps  ->  th )  <->  ( ch  ->  ta ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177
This theorem is referenced by:  nfbidf  1782  drnf1  2010  drnf2  2011  equveli  2025  ax11v2  2028  ax11vALT  2131  ax10-16  2225  ax11eq  2228  ax11el  2229  ax11inda  2235  ax11v2-o  2236  mobid  2273  2mo  2317  2eu6  2324  axext3  2371  ralcom2  2816  cbvralf  2870  cbvraldva2  2880  vtoclgaf  2960  vtocl2gaf  2962  vtocl3gaf  2964  rspct  2989  rspc  2990  ceqex  3010  ralab2  3043  mob2  3058  mob  3060  morex  3062  reu7  3073  reu8  3074  nelrdva  3087  cdeqim  3098  sbcimg  3146  csbhypf  3230  cbvralcsf  3255  dfss2f  3283  sbcss  3682  sneqrg  3911  elintab  4004  intss1  4008  intmin  4013  dfiin2g  4067  trel  4251  trss  4253  zfpow  4320  rext  4354  opth  4377  copsexg  4384  poeq1  4448  pocl  4452  swopolem  4454  swopo  4455  isso2i  4477  fri  4486  ordelord  4545  reusv2lem4  4668  reusv3i  4671  tfis  4775  tfisi  4779  tfindsg  4781  tfindsg2  4782  tfindes  4783  dfom2  4788  limomss  4791  nnlim  4799  findsg  4813  findes  4816  vtoclr  4863  poinxp  4882  posn  4887  ssrel  4905  ssrel2  4907  ssrelrel  4917  relop  4964  issref  5188  iota5  5379  funopg  5426  brprcneu  5662  tz6.12f  5690  funbrfv  5705  ssimaexg  5729  fvmptf  5761  fvelrn  5806  fprg  5855  f1veqaeq  5945  dff13f  5946  soisores  5987  soisoi  5988  isofrlem  6000  isopolem  6005  f1oweALT  6014  weniso  6015  oprabid  6045  ovmpt2s  6137  ov2gf  6138  ov3  6150  caovcan  6191  caovordig  6192  caofrss  6277  caoftrn  6279  dfoprab4f  6345  frxp  6393  poxp  6395  riota5f  6511  riotasv2d  6531  riotasv2dOLD  6532  onfununi  6540  smoel  6559  smogt  6566  tfrlem1  6573  tz7.48lem  6635  tz7.49  6639  oawordeu  6735  omordi  6746  oeordi  6767  nnmordi  6811  omabs  6827  nneob  6832  omsmolem  6833  qsel  6920  eroveu  6936  ecopovtrn  6944  th3qlem2  6948  ixpsnf1o  7039  fundmeng  7118  sbth  7164  limensuc  7221  nneneq  7227  php  7228  php2  7229  unxpdom  7253  pssnn  7264  findcard  7284  findcard2  7285  findcard3  7287  ac6sfi  7288  frfi  7289  domunfican  7316  fiint  7320  iunfi  7331  finsschain  7349  dffi3  7372  marypha1lem  7374  marypha1  7375  supmo  7391  suplub  7399  supisolem  7409  ordiso2  7418  ordtypelem7  7427  wemaplem1  7449  wemaplem2  7450  zfregcl  7496  inf0  7510  inf3lem1  7517  zfinf  7528  axinf2  7529  dfom3  7536  elom3  7537  cantnfval2  7558  cantnfle  7560  cantnflt  7561  cantnfp1lem3  7570  oemapvali  7574  cantnflem1c  7577  cantnflem1  7579  cantnf  7583  wemapwe  7588  cnfcom  7591  setind  7607  r1sdom  7634  r1ordg  7638  rankonidlem  7688  rankunb  7710  bnd2  7751  infxpenlem  7829  infxpenc2  7837  dfac8alem  7844  dfac8clem  7847  indcardi  7856  alephordi  7889  alephinit  7910  alephfp  7923  aceq3lem  7935  dfac5lem4  7941  dfac5  7943  dfac2  7945  dfac9  7950  dfac12lem2  7958  dfac12lem3  7959  kmlem1  7964  kmlem4  7967  kmlem10  7973  kmlem12  7975  kmlem13  7976  pwsdompw  8018  ackbij1lem16  8049  cfslb2n  8082  cfsmolem  8084  sornom  8091  fin2i  8109  infpssrlem4  8120  isfin2-2  8133  isfin3ds  8143  fin23lem17  8152  fin23lem32  8158  fin23lem34  8160  fin23lem35  8161  fin23lem39  8164  fin23lem41  8166  isf32lem2  8168  isf33lem  8180  isf34lem4  8191  isf34lem6  8194  fin1a2lem10  8223  axcc2lem  8250  axcc3  8252  axcc4dom  8255  dominf  8259  axdc2lem  8262  axdc3lem2  8265  ac6sg  8302  zorn2lem7  8316  zornn0g  8319  ttukeylem5  8327  ttukeylem6  8328  axdclem  8333  fodomg  8337  dominfac  8382  axrepndlem1  8401  axrepndlem2  8402  axunndlem1  8404  axunnd  8405  axpowndlem2  8407  axpowndlem3  8408  axpowndlem4  8409  axregndlem2  8412  axregnd  8413  axinfndlem1  8414  axinfnd  8415  axacndlem4  8419  axacndlem5  8420  axacnd  8421  zfcndpow  8425  zfcndinf  8427  fpwwe2lem5  8443  fpwwe2lem8  8446  fpwwe2lem12  8450  pwfseqlem4a  8470  pwfseqlem4  8471  pwfseqlem5  8472  pwfseq  8473  wunfi  8530  wunex2  8547  inar1  8584  rankcf  8586  tskord  8589  grudomon  8626  grur1a  8628  axgroth6  8637  axgroth3  8640  axgroth4  8641  eltskm  8652  indpi  8718  pinq  8738  nqereu  8740  prcdnq  8804  prnmax  8806  ltsopr  8843  prlem936  8858  ltsosr  8903  recexsrlem  8912  mulgt0sr  8914  map2psrpr  8919  supsrlem  8920  axrrecex  8972  axpre-lttrn  8975  axpre-mulgt0  8977  axpre-sup  8978  axsup  9085  ltordlem  9485  ltord1  9486  wloglei  9492  squeeze0  9846  infm3  9900  nnsub  9971  nnunb  10150  peano5uzti  10292  uzindOLD  10297  fzind  10301  eluzadd  10447  eluzsub  10448  uzind4s  10469  uzind4s2  10470  zmax  10504  zbtwnre  10505  xmulasslem  10797  xrsupsslem  10818  xrinfmsslem  10819  xrub  10823  injresinj  11128  om2uzlti  11218  uzindi  11248  axdc4uz  11250  seqp1  11266  seqcl2  11269  seqfveq2  11273  seqshft2  11277  monoord  11281  seqsplit  11284  seqf1olem2  11291  seqf1o  11292  seqid2  11297  seqhomo  11298  seqof2  11309  expcl2lem  11321  facdiv  11506  facwordi  11508  faclbnd4lem2  11513  hashnn0n0nn  11592  hashf1lem2  11633  seqcoll  11640  brfi1uzind  11643  wrdind  11719  rlim2  12218  ello1mpt  12243  rlimclim1  12267  o1co  12308  o1compt  12309  rlimcn1  12310  rlimcn2  12312  climcn1  12313  climcn2  12314  subcn2  12316  o1of2  12334  caucvgrlem  12394  fsum2d  12483  fsumabs  12508  fsumtscopo  12509  fsumrlim  12518  fsumo1  12519  o1fsum  12520  fsumiun  12528  rpnnen2lem10  12751  sqr2irr  12776  dvdsle  12823  divalglem7  12847  divalglem8  12848  ndvdssub  12855  gcdcllem1  12939  algcvg  12995  algcvga  12998  algfx  12999  isprm2lem  13014  prmind2  13018  dvdsprime  13020  nprm  13021  dvdsprm  13027  coprm  13028  coprmdvds2  13031  isprm6  13037  exprmfct  13038  prmfac1  13046  eulerthlem2  13099  pcqmul  13155  pcqcl  13158  pc2dvds  13180  pcz  13182  prmpwdvds  13200  infpn2  13209  vdwlem12  13288  ramub2  13310  rami  13311  ramcl  13325  prmlem0  13356  mreintcl  13748  ismred2  13756  mrissmrcd  13793  mreexexlemd  13797  iscatd2  13834  moni  13890  yoniso  14310  isprs  14315  prslem  14316  drsdirfi  14323  ispos  14332  posi  14335  isposd  14340  lubfval  14363  lubid  14367  glbfval  14368  joinle  14378  meetle  14385  isclat  14466  clatlem  14467  clatl  14471  lubl  14475  lubun  14478  clatleglb  14481  pospropd  14489  poslubmo  14501  ipodrsima  14519  acsdrsel  14521  isacs4lem  14522  isacs5lem  14523  acsdrscl  14524  mreclat  14541  pslem  14566  spwval2  14584  spwmo  14586  dirtr  14609  isnsg2  14898  ghmf1  14962  orbsta  15018  sylow1lem1  15160  sylow2alem2  15180  sylow2a  15181  lsmmod  15235  lsmdisj2  15242  efgsrel  15294  efgredlemd  15304  efgredlem  15307  efgred  15308  gsumzaddlem  15454  dprdval  15489  dprddisj2  15525  ablfac1eulem  15558  pgpfac1lem1  15560  pgpfac1lem5  15565  pgpfac1  15566  pgpfaclem2  15568  pgpfac  15570  irredmul  15742  isdrngrd  15789  islbs3  16155  rrgval  16275  rrgeq0i  16277  isdomn  16282  domneq0  16285  mplsubglem  16426  mpllsslem  16427  mplcoe1  16456  mplcoe2  16458  prmirredlem  16697  znfld  16765  znrrg  16770  cygznlem3  16774  isphl  16783  ipeq0  16793  isphld  16809  phlpropd  16810  lsmcss  16843  uniopn  16894  fiinopn  16898  epttop  16997  clsndisj  17063  elcls3  17071  neiptoptop  17119  neiptopnei  17120  cnpval  17223  iscnp  17224  cnpimaex  17243  lmcvg  17249  cnprest  17276  cnprest2  17277  lmss  17285  lmff  17288  ist1  17308  t0sep  17311  hausnei  17315  isnrm2  17345  t1sep2  17356  isreg2  17364  iscmp  17374  cmpcov  17375  cmpsublem  17385  cmpsub  17386  tgcmp  17387  uncmp  17389  fiuncmp  17390  hauscmplem  17392  cmpfi  17394  cmpfii  17395  dfcon2  17404  consuba  17405  connsub  17406  nconsubb  17408  1stcclb  17429  1stcfb  17430  2ndc1stc  17436  1stcrest  17438  1stcelcls  17446  restnlly  17467  lly1stc  17481  kgenval  17489  kgeni  17491  kgencn2  17511  ptcldmpt  17568  ptclsg  17569  dfac14lem  17571  dfac14  17572  txcnp  17574  ptcnp  17576  hausdiag  17599  txlm  17602  tx1stc  17604  xkococn  17614  cnmpt12  17621  cnmpt22  17628  kqt0lem  17690  isr0  17691  regr1lem2  17694  kqreglem1  17695  r0sep  17702  ptcmpfi  17767  elmptrab  17781  isfil  17801  filss  17807  isufil2  17862  cfinufil  17882  rnelfm  17907  fmfnfmlem2  17909  fmfnfmlem4  17911  flimopn  17929  flimrest  17937  flftg  17950  cnpflf  17955  txflf  17960  fclsopni  17969  fclsrest  17978  fclscf  17979  flimfnfcls  17982  fcfnei  17989  alexsublem  17997  alexsubb  17999  alexsubALTlem3  18002  alexsubALTlem4  18003  alexsubALT  18004  cnextcn  18020  cnextfres  18021  tgpt0  18070  divstgplem  18072  tsmsi  18085  tsmssubm  18094  tsmsres  18095  tsmsf1o  18096  tsmsxp  18106  ustssel  18157  ust0  18171  ustuqtop4  18196  ucnima  18233  ucncn  18237  iscusp  18251  cuspcvg  18253  imasdsf1olem  18312  blss  18347  metss  18429  comet  18434  metcnp3  18461  metcnp2  18463  txmetcnp  18468  metuel2  18486  metucn  18491  nrmmetd  18494  nlmvscn  18595  nrginvrcn  18599  nmolb  18623  xrge0tsms  18737  divcn  18770  fsumcn  18772  elcncf2  18792  cncfi  18796  mulc1cncf  18807  cncfco  18809  cncfmet  18810  xrhmeo  18843  bndth  18855  nmoleub2lem2  18996  nmoleub3  18999  ipcn  19072  lmmbr  19083  caucfil  19108  pmltpc  19215  ovolfiniun  19265  ovolicc2lem3  19283  ovolicc2  19286  mblsplit  19296  finiunmbl  19306  volfiniun  19309  voliunlem3  19314  ioorinv  19336  ioorcl  19337  dyadmax  19358  dyadmbllem  19359  dyadmbl  19360  opnmbllem  19361  volcn  19366  vitalilem2  19369  vitalilem3  19370  vitali  19373  i1fd  19441  itg2seq  19502  itg2addlem  19518  itgfsum  19586  ellimc3  19634  dvbsss  19657  dvnres  19685  dvmptfsum  19727  dvferm1lem  19736  dvferm2lem  19738  rolle  19742  c1lip1  19749  lhop1lem  19765  lhop1  19766  dvfsumlem2  19779  dvfsumlem4  19781  dvfsumrlim  19783  dvfsum2  19786  ftc1a  19789  ftc1lem4  19791  ftc1lem6  19793  mpfind  19833  pf1ind  19843  mdegleb  19855  mdeglt  19856  deg1leb  19886  deg1lt  19888  ply1divex  19927  fta1glem2  19957  fta1g  19958  plyco0  19979  plyeq0lem  19997  coeeq2  20029  dgrle  20030  dgrcolem2  20060  dgrco  20061  plydivlem4  20081  plydivex  20082  fta1lem  20092  fta1  20093  vieta1lem2  20096  vieta1  20097  aalioulem2  20118  aalioulem4  20120  abelth  20225  cxpcn3  20500  rlimcnp  20672  xrlimcnp  20675  cxploglim  20684  scvxcvx  20692  jensen  20695  wilthlem2  20720  wilthlem3  20721  fta  20730  dvdsmulf1o  20847  perfectlem2  20882  dchrelbas3  20890  dchrelbas4  20895  dchrn0  20902  bcmono  20929  lgsdir2lem4  20978  lgsdchr  21000  lgseisenlem2  21002  lgsquad2lem2  21011  2sqlem6  21021  2sqlem8  21024  2sqlem10  21026  dchrisumlema  21050  dchrisumlem2  21052  dchrisumlem3  21053  nbusgra  21307  wlkntrllem5  21418  1pthoncl  21441  2pthoncl  21452  fargshiftf1  21473  constr3trllem2  21487  eupatrl  21539  eupath2  21551  isass  21753  ismgm  21757  isexid2  21762  nvz  22007  nmobndseqi  22129  nmobndseqiOLD  22130  nmlno0  22145  blocnilem  22154  dipdir  22192  dipass  22195  siilem2  22202  ubthlem2  22222  ubth  22224  htth  22270  normpyth  22496  norm3lemt  22503  chlimi  22586  chcompl  22594  omlsii  22754  pjoml  22787  h1de2i  22904  elspansn2  22918  h1datom  22933  pjoml2  22962  pjoml3  22963  lecm  22968  chscllem2  22989  osum  22996  spansncv  23004  pjcjt2  23043  pjopyth  23071  eigre  23187  eigorth  23190  hhcno  23256  hhcnf  23257  cnopc  23265  cnfnc  23282  nmcexi  23378  nmcopexi  23379  nmcfnexi  23403  pjssge0i  23518  hstel2  23571  stj  23587  stri  23609  hstri  23617  stcltr1i  23626  mdbr  23646  mdi  23647  mdbr3  23649  mdbr4  23650  dmdbr  23651  dmdmd  23652  dmdi  23654  dmdbr3  23657  dmdbr4  23658  dmdbr5  23660  mdsl1i  23673  mdslmd1lem3  23679  mdslmd1lem4  23680  mdslmd1i  23681  csmdsymi  23686  cvmd  23688  atss  23698  atom1d  23705  chcv1  23707  hatomic  23712  atord  23740  atcvat2  23741  mddmdin0i  23783  rmoxfrdOLD  23824  rmoxfrd  23825  ifeqeqx  23846  ssiun2sf  23855  fmptcof2  23919  resspos  24027  xrge0tsmsd  24053  isofld  24062  ofldadd  24065  ofldmul  24066  kerf1hrm  24079  xrge0iifiso  24126  esumcvg  24273  isrnsigaOLD  24292  sigaclcu  24297  sigaclci  24312  unelsiga  24314  measvun  24358  measiun  24367  lgamgulmlem2  24594  subfacp1lem6  24651  erdszelem9  24665  kur14lem9  24680  sconpht  24696  cvmsss2  24741  cvmliftlem7  24758  cvmliftlem10  24761  ghomf1olem  24885  relexpsucr  24910  relexpsucl  24912  relexpcnv  24913  relexpdm  24915  relexprn  24916  relexpadd  24918  relexpindlem  24919  rtrclreclem.min  24927  iota5f  24962  dedekind  24967  prodfdiv  25004  dfpo2  25137  fununiq  25151  setinds  25159  dfon2lem3  25166  dfon2lem4  25167  dfon2lem5  25168  dfon2lem6  25169  dfon2lem7  25170  dfon2lem8  25171  dfon2  25173  predbrg  25211  preddowncl  25221  tfisg  25229  wfisg  25234  frmin  25267  frinsg  25270  wfrlem9  25289  frrlem5e  25314  nocvxminlem  25369  axcgrtr  25569  btwnconn1lem11  25746  linethru  25802  rankelg  25824  rankeq1o  25827  voliunnfl  25956  volsupnfl  25957  itg2addnc  25960  itg2gt0cn  25961  ftc1cnnclem  25979  ftc1cnnc  25980  subtr  26009  subtr2  26010  trer  26011  nn0prpwlem  26017  nn0prpw  26018  comppfsc  26079  neibastop2lem  26081  filnetlem4  26102  f1opr  26118  sdclem2  26138  fdc  26141  fdc1  26142  neificl  26151  mettrifi  26155  sstotbnd2  26175  cntotbnd  26197  heibor1lem  26210  bfp  26225  iscringd  26301  ispridl  26336  pridl  26339  ismaxidl  26342  maxidlmax  26345  ispridlc  26372  pridlc  26373  dmnnzd  26377  ismrcd1  26444  ismrcd2  26445  ismrc  26447  isnacs3  26456  nacsfix  26458  mzpcompact2  26501  fphpd  26569  fphpdo  26570  monotuz  26696  monotoddzzfi  26697  monotoddzz  26698  oddcomabszz  26699  zindbi  26701  setindtrs  26788  dford3lem2  26790  ttac  26799  dnnumch1  26811  fnwe2lem2  26818  aomclem3  26823  aomclem6  26826  supeq123d  26828  aomclem8  26829  dfac11  26830  dfac21  26834  islssfg2  26839  frlmup1  26920  lindfrn  26961  islindf4  26978  islindf5  26979  hbtlem5  27002  hbt  27004  flcidc  27049  symggen  27081  psgnunilem4  27090  mendlmod  27171  sdrgacs  27179  pm14.122b  27293  sbiota1  27304  fnchoice  27369  fmul01  27379  fmulcl  27380  fmuldfeqlem1  27381  fmuldfeq  27382  fmul01lt1lem1  27383  fmul01lt1lem2  27384  climmulf  27399  climexp  27400  climsuse  27403  climrecf  27404  climinff  27406  stoweidlem3  27421  stoweidlem4  27422  stoweidlem6  27424  stoweidlem8  27426  stoweidlem15  27433  stoweidlem16  27434  stoweidlem17  27435  stoweidlem19  27437  stoweidlem20  27438  stoweidlem22  27440  stoweidlem23  27441  stoweidlem26  27444  stoweidlem27  27445  stoweidlem30  27448  stoweidlem31  27449  stoweidlem32  27450  stoweidlem34  27452  stoweidlem35  27453  stoweidlem42  27460  stoweidlem43  27461  stoweidlem48  27466  stoweidlem50  27468  stoweidlem51  27469  stoweidlem57  27475  stoweidlem59  27477  stoweidlem62  27480  wallispilem3  27485  sbcfun  27656  frgra3vlem1  27754  3vfriswmgralem  27758  3vfriswmgra  27759  frgrawopreglem4  27800  imbi12  27947  sbcssOLD  27971  bnj1385  28543  bnj110  28568  bnj222  28593  bnj229  28594  bnj590  28620  bnj865  28633  bnj849  28635  bnj981  28660  bnj1014  28670  bnj1015  28671  bnj1112  28691  bnj1118  28692  bnj1123  28694  bnj1128  28698  bnj1125  28700  bnj1148  28704  bnj1154  28707  bnj1326  28734  bnj1384  28740  bnj1489  28764  bnj1497  28768  drnf1NEW7  28834  drnf2wAUX7  28837  drnf2w2AUX7  28840  drnf2w3AUX7  28843  equveliNEW7  28865  ax11v2NEW7  28867  drnf2OLD7  29033  lubunNEW  29089  lshpdisj  29103  lsmsatcv  29126  lsat0cv  29149  lcvexchlem4  29153  lcvexchlem5  29154  l1cvpat  29170  isopos  29296  oposlem  29299  isoml  29354  omllaw  29359  isatl  29415  atlex  29432  iscvlat  29439  cvlexch1  29444  glbconN  29492  hlsuprexch  29496  ps-1  29592  3atlem5  29602  psubspi  29862  llnexchb2  29984  elpcliN  30008  pclfinclN  30065  ldilval  30228  ltrnfset  30232  ltrnset  30233  ltrnu  30236  trlfset  30275  trlset  30276  trlval2  30278  cdleme25cv  30473  cdleme31so  30494  cdleme31fv  30505  cdlemefrs29bpre0  30511  cdleme32fva  30552  cdleme40v  30584  trlord  30684  cdlemkid3N  31048  cdlemkid4  31049  dihffval  31346  dihfval  31347  dihval  31348  lpolconN  31603  mapdordlem2  31753  hdmapfval  31946  hdmapval  31947  hdmapval2  31951
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 178
  Copyright terms: Public domain W3C validator