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

Theorem imbi12d 311
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 308 . 2  |-  ( ph  ->  ( ( ps  ->  th )  <->  ( ch  ->  th ) ) )
3 imbi12d.2 . . 3  |-  ( ph  ->  ( th  <->  ta )
)
43imbi2d 307 . 2  |-  ( ph  ->  ( ( ch  ->  th )  <->  ( ch  ->  ta ) ) )
52, 4bitrd 244 1  |-  ( ph  ->  ( ( ps  ->  th )  <->  ( ch  ->  ta ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176
This theorem is referenced by:  nfbidf  1766  drnf1  1922  drnf2  1923  equveli  1941  ax11v2  1945  ax10-16  2142  ax11eq  2145  ax11el  2146  ax11inda  2152  ax11v2-o  2153  mobid  2190  2mo  2234  2eu6  2241  axext3  2279  ralcom2  2717  cbvralf  2771  cbvraldva2  2781  vtoclgaf  2861  vtocl2gaf  2863  vtocl3gaf  2865  rspct  2890  rspc  2891  ceqex  2911  ralab2  2943  mob2  2958  mob  2960  morex  2962  reu7  2973  reu8  2974  cdeqim  2997  sbcimg  3045  csbhypf  3129  cbvralcsf  3156  dfss2f  3184  sbcss  3577  sneqrg  3798  elintab  3889  intss1  3893  intmin  3898  dfiin2g  3952  trel  4136  trss  4138  zfpow  4205  rext  4238  opth  4261  copsexg  4268  poeq1  4333  pocl  4337  swopolem  4339  swopo  4340  isso2i  4362  fri  4371  ordelord  4430  reusv2lem4  4554  reusv3i  4557  tfis  4661  tfisi  4665  tfindsg  4667  tfindsg2  4668  tfindes  4669  dfom2  4674  limomss  4677  nnlim  4685  findsg  4699  findes  4702  vtoclr  4749  poinxp  4769  posn  4774  ssrel  4792  ssrelrel  4803  relop  4850  issref  5072  iota5  5255  funopg  5302  brprcneu  5534  tz6.12f  5562  funbrfv  5577  ssimaexg  5601  fvmptf  5632  fvelrn  5677  dff13f  5800  f1fveq  5802  soisores  5840  soisoi  5841  isofrlem  5853  isopolem  5858  f1oweALT  5867  weniso  5868  oprabid  5898  ovmpt2s  5987  ov2gf  5988  ov3  6000  caovcan  6040  caovordig  6041  caofrss  6126  caoftrn  6128  dfoprab4f  6194  frxp  6241  poxp  6243  riota5f  6345  riotasv2d  6365  riotasv2dOLD  6366  onfununi  6374  smoel  6393  smogt  6400  tfrlem1  6407  tz7.48lem  6469  tz7.49  6473  oawordeu  6569  omordi  6580  oeordi  6601  nnmordi  6645  omabs  6661  nneob  6666  omsmolem  6667  qsel  6754  eroveu  6769  ecopovtrn  6777  th3qlem2  6781  ixpsnf1o  6872  fundmeng  6951  sbth  6997  limensuc  7054  nneneq  7060  php  7061  php2  7062  unxpdom  7086  pssnn  7097  findcard  7113  findcard2  7114  findcard3  7116  ac6sfi  7117  frfi  7118  domunfican  7145  fiint  7149  iunfi  7160  finsschain  7178  dffi3  7200  marypha1lem  7202  marypha1  7203  supmo  7219  suplub  7227  supisolem  7237  ordiso2  7246  ordtypelem7  7255  wemaplem1  7277  wemaplem2  7278  zfregcl  7324  inf0  7338  inf3lem1  7345  zfinf  7356  axinf2  7357  dfom3  7364  elom3  7365  cantnfval2  7386  cantnfle  7388  cantnflt  7389  cantnfp1lem3  7398  oemapvali  7402  cantnflem1c  7405  cantnflem1  7407  cantnf  7411  wemapwe  7416  cnfcom  7419  setind  7435  r1sdom  7462  r1ordg  7466  rankonidlem  7516  rankunb  7538  bnd2  7579  infxpenlem  7657  infxpenc2  7665  dfac8alem  7672  dfac8clem  7675  indcardi  7684  alephordi  7717  alephinit  7738  alephfp  7751  aceq3lem  7763  dfac5lem4  7769  dfac5  7771  dfac2  7773  dfac9  7778  dfac12lem2  7786  dfac12lem3  7787  kmlem1  7792  kmlem4  7795  kmlem10  7801  kmlem12  7803  kmlem13  7804  pwsdompw  7846  ackbij1lem16  7877  cfslb2n  7910  cfsmolem  7912  sornom  7919  fin2i  7937  infpssrlem4  7948  isfin2-2  7961  isfin3ds  7971  fin23lem17  7980  fin23lem32  7986  fin23lem34  7988  fin23lem35  7989  fin23lem39  7992  fin23lem41  7994  isf32lem2  7996  isf33lem  8008  isf34lem4  8019  isf34lem6  8022  fin1a2lem10  8051  axcc2lem  8078  axcc3  8080  axcc4dom  8083  dominf  8087  axdc2lem  8090  axdc3lem2  8093  ac6sg  8131  zorn2lem7  8145  zornn0g  8148  ttukeylem5  8156  ttukeylem6  8157  axdclem  8162  fodomg  8166  dominfac  8211  axrepndlem1  8230  axrepndlem2  8231  axunndlem1  8233  axunnd  8234  axpowndlem2  8236  axpowndlem3  8237  axpowndlem4  8238  axregndlem2  8241  axregnd  8242  axinfndlem1  8243  axinfnd  8244  axacndlem4  8248  axacndlem5  8249  axacnd  8250  zfcndpow  8254  zfcndinf  8256  fpwwe2lem5  8272  fpwwe2lem8  8275  fpwwe2lem12  8279  pwfseqlem4a  8299  pwfseqlem4  8300  pwfseqlem5  8301  pwfseq  8302  wunfi  8359  wunex2  8376  inar1  8413  rankcf  8415  tskord  8418  grudomon  8455  grur1a  8457  axgroth6  8466  axgroth3  8469  axgroth4  8470  eltskm  8481  indpi  8547  pinq  8567  nqereu  8569  prcdnq  8633  prnmax  8635  ltsopr  8672  prlem936  8687  ltsosr  8732  recexsrlem  8741  mulgt0sr  8743  map2psrpr  8748  supsrlem  8749  axrrecex  8801  axpre-lttrn  8804  axpre-mulgt0  8806  axpre-sup  8807  axsup  8914  ltordlem  9314  ltord1  9315  wloglei  9321  squeeze0  9675  infm3  9729  nnsub  9800  nnunb  9977  peano5uzti  10117  uzindOLD  10122  fzind  10126  eluzadd  10272  eluzsub  10273  uzind4s  10294  uzind4s2  10295  zmax  10329  zbtwnre  10330  xmulasslem  10621  xrsupsslem  10641  xrinfmsslem  10642  xrub  10646  om2uzlti  11029  uzindi  11059  axdc4uz  11061  seqp1  11077  seqcl2  11080  seqfveq2  11084  seqshft2  11088  monoord  11092  seqsplit  11095  seqf1olem2  11102  seqf1o  11103  seqid2  11108  seqhomo  11109  expcl2lem  11131  facdiv  11316  facwordi  11318  faclbnd4lem2  11323  hashf1lem2  11410  seqcoll  11417  wrdind  11493  rlim2  11986  ello1mpt  12011  rlimclim1  12035  o1co  12076  o1compt  12077  rlimcn1  12078  rlimcn2  12080  climcn1  12081  climcn2  12082  subcn2  12084  o1of2  12102  caucvgrlem  12161  fsum2d  12250  fsumabs  12275  fsumtscopo  12276  fsumrlim  12285  fsumo1  12286  o1fsum  12287  fsumiun  12295  rpnnen2lem10  12518  sqr2irr  12543  dvdsle  12590  divalglem7  12614  divalglem8  12615  ndvdssub  12622  gcdcllem1  12706  algcvg  12762  algcvga  12765  algfx  12766  isprm2lem  12781  prmind2  12785  dvdsprime  12787  nprm  12788  dvdsprm  12794  coprm  12795  coprmdvds2  12798  isprm6  12804  exprmfct  12805  prmfac1  12813  eulerthlem2  12866  pcqmul  12922  pcqcl  12925  pc2dvds  12947  pcz  12949  prmpwdvds  12967  infpn2  12976  vdwlem12  13055  ramub2  13077  rami  13078  ramcl  13092  prmlem0  13123  mreintcl  13513  ismred2  13521  mrissmrcd  13558  mreexexlemd  13562  iscatd2  13599  moni  13655  yoniso  14075  isprs  14080  prslem  14081  drsdirfi  14088  ispos  14097  posi  14100  isposd  14105  lubfval  14128  lubid  14132  glbfval  14133  joinle  14143  meetle  14150  isclat  14231  clatlem  14232  clatl  14236  lubl  14240  lubun  14243  clatleglb  14246  pospropd  14254  poslubmo  14266  ipodrsima  14284  acsdrsel  14286  isacs4lem  14287  isacs5lem  14288  acsdrscl  14289  mreclat  14306  pslem  14331  spwval2  14349  spwmo  14351  dirtr  14374  isnsg2  14663  ghmf1  14727  orbsta  14783  sylow1lem1  14925  sylow2alem2  14945  sylow2a  14946  lsmmod  15000  lsmdisj2  15007  efgsrel  15059  efgredlemd  15069  efgredlem  15072  efgred  15073  gsumzaddlem  15219  dprdval  15254  dprddisj2  15290  ablfac1eulem  15323  pgpfac1lem1  15325  pgpfac1lem5  15330  pgpfac1  15331  pgpfaclem2  15333  pgpfac  15335  irredmul  15507  isdrngrd  15554  islbs3  15924  rrgval  16044  rrgeq0i  16046  isdomn  16051  domneq0  16054  mplsubglem  16195  mpllsslem  16196  mplcoe1  16225  mplcoe2  16227  prmirredlem  16462  znfld  16530  znrrg  16535  cygznlem3  16539  isphl  16548  ipeq0  16558  isphld  16574  phlpropd  16575  lsmcss  16608  uniopn  16659  fiinopn  16663  epttop  16762  clsndisj  16828  elcls3  16836  cnpval  16982  iscnp  16983  cnpimaex  17002  lmcvg  17008  cnprest  17033  cnprest2  17034  lmss  17042  lmff  17045  ist1  17065  t0sep  17068  hausnei  17072  isnrm2  17102  t1sep2  17113  isreg2  17121  iscmp  17131  cmpcov  17132  cmpsublem  17142  cmpsub  17143  tgcmp  17144  uncmp  17146  fiuncmp  17147  hauscmplem  17149  cmpfi  17151  cmpfii  17152  dfcon2  17161  consuba  17162  connsub  17163  nconsubb  17165  1stcclb  17186  1stcfb  17187  2ndc1stc  17193  1stcrest  17195  1stcelcls  17203  restnlly  17224  lly1stc  17238  kgenval  17246  kgeni  17248  kgencn2  17268  ptcldmpt  17324  ptclsg  17325  dfac14lem  17327  dfac14  17328  txcnp  17330  ptcnp  17332  hausdiag  17355  txlm  17358  tx1stc  17360  xkococn  17370  cnmpt12  17377  cnmpt22  17384  kqt0lem  17443  isr0  17444  regr1lem2  17447  kqreglem1  17448  r0sep  17455  ptcmpfi  17520  elmptrab  17538  isfil  17558  filss  17564  isufil2  17619  cfinufil  17639  rnelfm  17664  fmfnfmlem2  17666  fmfnfmlem4  17668  flimopn  17686  flimrest  17694  flftg  17707  cnpflf  17712  txflf  17717  fclsopni  17726  fclsrest  17735  fclscf  17736  flimfnfcls  17739  fcfnei  17746  alexsublem  17754  alexsubb  17756  alexsubALTlem3  17759  alexsubALTlem4  17760  alexsubALT  17761  tgpt0  17817  divstgplem  17819  tsmsi  17832  tsmssubm  17841  tsmsres  17842  tsmsf1o  17843  tsmsxp  17853  imasdsf1olem  17953  blss  17988  metss  18070  comet  18075  metcnp3  18102  metcnp2  18104  txmetcnp  18109  nrmmetd  18113  nlmvscn  18214  nrginvrcn  18218  nmolb  18242  xrge0tsms  18355  divcn  18388  fsumcn  18390  elcncf2  18410  cncfi  18414  mulc1cncf  18425  cncfco  18427  cncfmet  18428  xrhmeo  18460  bndth  18472  nmoleub2lem2  18613  nmoleub3  18616  ipcn  18689  lmmbr  18700  caucfil  18725  pmltpc  18826  ovolfiniun  18876  ovolicc2lem3  18894  ovolicc2  18897  mblsplit  18907  finiunmbl  18917  volfiniun  18920  voliunlem3  18925  ioorinv  18947  ioorcl  18948  dyadmax  18969  dyadmbllem  18970  dyadmbl  18971  opnmbllem  18972  volcn  18977  vitalilem2  18980  vitalilem3  18981  vitali  18984  i1fd  19052  itg2seq  19113  itg2addlem  19129  itgfsum  19197  ellimc3  19245  dvbsss  19268  dvnres  19296  dvmptfsum  19338  dvferm1lem  19347  dvferm2lem  19349  rolle  19353  c1lip1  19360  lhop1lem  19376  lhop1  19377  dvfsumlem2  19390  dvfsumlem4  19392  dvfsumrlim  19394  dvfsum2  19397  ftc1a  19400  ftc1lem4  19402  ftc1lem6  19404  mpfind  19444  pf1ind  19454  mdegleb  19466  mdeglt  19467  deg1leb  19497  deg1lt  19499  ply1divex  19538  fta1glem2  19568  fta1g  19569  plyco0  19590  plyeq0lem  19608  coeeq2  19640  dgrle  19641  dgrcolem2  19671  dgrco  19672  plydivlem4  19692  plydivex  19693  fta1lem  19703  fta1  19704  vieta1lem2  19707  vieta1  19708  aalioulem2  19729  aalioulem4  19731  abelth  19833  cxpcn3  20104  rlimcnp  20276  xrlimcnp  20279  cxploglim  20288  scvxcvx  20296  jensen  20299  wilthlem2  20323  wilthlem3  20324  fta  20333  dvdsmulf1o  20450  perfectlem2  20485  dchrelbas3  20493  dchrelbas4  20498  dchrn0  20505  bcmono  20532  lgsdir2lem4  20581  lgsdchr  20603  lgseisenlem2  20605  lgsquad2lem2  20614  2sqlem6  20624  2sqlem8  20627  2sqlem10  20629  dchrisumlema  20653  dchrisumlem2  20655  dchrisumlem3  20656  isass  20999  ismgm  21003  isexid2  21008  nvz  21251  nmobndseqi  21373  nmobndseqiOLD  21374  nmlno0  21389  blocnilem  21398  dipdir  21436  dipass  21439  siilem2  21446  ubthlem2  21466  ubth  21468  htth  21514  normpyth  21740  norm3lemt  21747  chlimi  21830  chcompl  21838  omlsii  21998  pjoml  22031  h1de2i  22148  elspansn2  22162  h1datom  22177  pjoml2  22206  pjoml3  22207  lecm  22212  chscllem2  22233  osum  22240  spansncv  22248  pjcjt2  22287  pjopyth  22315  eigre  22431  eigorth  22434  hhcno  22500  hhcnf  22501  cnopc  22509  cnfnc  22526  nmcexi  22622  nmcopexi  22623  nmcfnexi  22647  pjssge0i  22762  hstel2  22815  stj  22831  stri  22853  hstri  22861  stcltr1i  22870  mdbr  22890  mdi  22891  mdbr3  22893  mdbr4  22894  dmdbr  22895  dmdmd  22896  dmdi  22898  dmdbr3  22901  dmdbr4  22902  dmdbr5  22904  mdsl1i  22917  mdslmd1lem3  22923  mdslmd1lem4  22924  mdslmd1i  22925  csmdsymi  22930  cvmd  22932  atss  22942  atom1d  22949  chcv1  22951  hatomic  22956  atord  22984  atcvat2  22985  mddmdin0i  23027  ifeqeqx  23050  rmoxfrdOLD  23162  rmoxfrd  23163  ssiun2sf  23173  fmptcof2  23244  xrge0iifiso  23332  xrge0tsmsd  23397  esumcvg  23469  isrnsigaOLD  23488  sigaclcu  23493  sigaclci  23508  unelsiga  23510  measvun  23552  measiun  23560  subfacp1lem6  23731  erdszelem9  23745  kur14lem9  23760  sconpht  23775  cvmsss2  23820  cvmliftlem7  23837  cvmliftlem10  23840  eupath2  23919  ghomf1olem  24016  relexpsucr  24041  relexpsucl  24043  relexpcnv  24044  relexpdm  24047  relexprn  24048  relexpadd  24050  relexpindlem  24051  rtrclreclem.min  24059  dedekind  24097  dfpo2  24183  fununiq  24197  setinds  24205  dfon2lem3  24212  dfon2lem4  24213  dfon2lem5  24214  dfon2lem6  24215  dfon2lem7  24216  dfon2lem8  24217  dfon2  24219  predbrg  24257  preddowncl  24267  tfisg  24275  wfisg  24280  frmin  24313  frinsg  24316  wfrlem9  24335  frrlem5e  24360  nocvxminlem  24415  axcgrtr  24615  btwnconn1lem11  24792  linethru  24848  rankelg  24870  rankeq1o  24873  itg2addnc  25005  itg2gt0cn  25006  ftc1cnnclem  25024  ftc1cnnc  25025  fprg  25236  cbcpcp  25265  prjmapcp2  25273  isorhom  25314  preoref22  25332  preotr2  25338  mxlelt  25367  ismxl2  25370  ismnl2  25371  defge3  25374  defse3  25375  inposet  25381  iscom  25436  idlvalNEW  25548  svli2  25587  osneisi  25634  istopx  25650  bwt2  25695  supnuf  25732  supexr  25734  cnegvex2b  25765  rnegvex2b  25766  intvconlem1  25806  isded  25839  dedi  25840  domcmpd  25849  codcmpd  25850  iscatOLD  25857  cati  25858  cmpasso  25876  cmpida  25877  cmpidb  25878  ishomd  25893  ismona  25912  ismonb  25913  ismonb2  25915  cmpmon  25918  isepia  25922  isepib  25923  isepib2  25925  isfuna  25937  isinob  25965  islimcat  25979  tartarmap  25991  rocatval2  26063  setiscat  26082  clscnc  26113  pgapspf2  26156  isig2a2  26169  isibg2  26213  isibg2aa  26215  isibg2aalem1  26216  isibg2aalem2  26217  isibg2aalem3  26218  segline  26244  isibcg  26294  subtr  26327  subtr2  26328  trer  26330  nn0prpwlem  26341  nn0prpw  26342  comppfsc  26410  neibastop2lem  26412  filnetlem4  26433  f1opr  26494  sdclem2  26555  fdc  26558  fdc1  26559  neificl  26570  mettrifi  26576  sstotbnd2  26601  cntotbnd  26623  heibor1lem  26636  bfp  26651  iscringd  26727  ispridl  26762  pridl  26765  ismaxidl  26768  maxidlmax  26771  ispridlc  26798  pridlc  26799  dmnnzd  26803  ismrcd1  26876  ismrcd2  26877  ismrc  26879  isnacs3  26888  nacsfix  26890  mzpcompact2  26933  fphpd  27002  fphpdo  27003  monotuz  27129  monotoddzzfi  27130  monotoddzz  27131  oddcomabszz  27132  zindbi  27134  setindtrs  27221  dford3lem2  27223  ttac  27232  dnnumch1  27244  fnwe2lem2  27251  aomclem3  27256  aomclem6  27259  supeq123d  27261  aomclem8  27262  dfac11  27263  dfac21  27267  islssfg2  27272  frlmup1  27353  lindfrn  27394  islindf4  27411  islindf5  27412  hbtlem5  27435  hbt  27437  flcidc  27482  symggen  27514  psgnunilem4  27523  mendlmod  27604  sdrgacs  27612  pm14.122b  27726  sbiota1  27737  fnchoice  27803  fmul01  27813  fmulcl  27814  fmuldfeqlem1  27815  fmuldfeq  27816  fmul01lt1lem1  27817  fmul01lt1lem2  27818  climmulf  27833  climexp  27834  climsuse  27837  climrecf  27838  climinff  27840  stoweidlem3  27855  stoweidlem4  27856  stoweidlem6  27858  stoweidlem8  27860  stoweidlem15  27867  stoweidlem16  27868  stoweidlem17  27869  stoweidlem19  27871  stoweidlem20  27872  stoweidlem22  27874  stoweidlem23  27875  stoweidlem26  27878  stoweidlem27  27879  stoweidlem30  27882  stoweidlem31  27883  stoweidlem32  27884  stoweidlem34  27886  stoweidlem35  27887  stoweidlem42  27894  stoweidlem43  27895  stoweidlem48  27900  stoweidlem50  27902  stoweidlem51  27903  stoweidlem57  27909  stoweidlem59  27911  stoweidlem62  27914  wallispilem3  27919  sbcfun  28090  f1veqaeq  28188  injresinj  28215  nbusgra  28277  wlkntrllem5  28349  fargshiftf1  28382  eupatrl  28385  constr3trllem2  28397  frgra3vlem1  28424  3vfriswmgralem  28428  3vfriswmgra  28429  imbi12  28581  sbcssOLD  28605  bnj1385  29181  bnj110  29206  bnj222  29231  bnj229  29232  bnj590  29258  bnj865  29271  bnj849  29273  bnj981  29298  bnj1014  29308  bnj1015  29309  bnj1112  29329  bnj1118  29330  bnj1123  29332  bnj1128  29336  bnj1125  29338  bnj1148  29342  bnj1154  29345  bnj1326  29372  bnj1384  29378  bnj1489  29402  bnj1497  29406  drnf1NEW7  29472  drnf2wAUX7  29475  drnf2w2AUX7  29478  drnf2w3AUX7  29481  equveliNEW7  29503  ax11v2NEW7  29505  drnf2OLD7  29670  a12lem1  29752  lubunNEW  29785  lshpdisj  29799  lsmsatcv  29822  lsat0cv  29845  lcvexchlem4  29849  lcvexchlem5  29850  l1cvpat  29866  isopos  29992  oposlem  29995  isoml  30050  omllaw  30055  isatl  30111  atlex  30128  iscvlat  30135  cvlexch1  30140  glbconN  30188  hlsuprexch  30192  ps-1  30288  3atlem5  30298  psubspi  30558  llnexchb2  30680  elpcliN  30704  pclfinclN  30761  ldilval  30924  ltrnfset  30928  ltrnset  30929  ltrnu  30932  trlfset  30971  trlset  30972  trlval2  30974  cdleme25cv  31169  cdleme31so  31190  cdleme31fv  31201  cdlemefrs29bpre0  31207  cdleme32fva  31248  cdleme40v  31280  trlord  31380  cdlemkid3N  31744  cdlemkid4  31745  dihffval  32042  dihfval  32043  dihval  32044  lpolconN  32299  mapdordlem2  32449  hdmapfval  32642  hdmapval  32643  hdmapval2  32647
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