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

Theorem 3bitr4d 278
Description: Deduction from transitivity of biconditional. Useful for converting conditional definitions in a formula. (Contributed by NM, 18-Oct-1995.)
Hypotheses
Ref Expression
3bitr4d.1  |-  ( ph  ->  ( ps  <->  ch )
)
3bitr4d.2  |-  ( ph  ->  ( th  <->  ps )
)
3bitr4d.3  |-  ( ph  ->  ( ta  <->  ch )
)
Assertion
Ref Expression
3bitr4d  |-  ( ph  ->  ( th  <->  ta )
)

Proof of Theorem 3bitr4d
StepHypRef Expression
1 3bitr4d.2 . 2  |-  ( ph  ->  ( th  <->  ps )
)
2 3bitr4d.1 . . 3  |-  ( ph  ->  ( ps  <->  ch )
)
3 3bitr4d.3 . . 3  |-  ( ph  ->  ( ta  <->  ch )
)
42, 3bitr4d 249 . 2  |-  ( ph  ->  ( ps  <->  ta )
)
51, 4bitrd 246 1  |-  ( ph  ->  ( th  <->  ta )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 178
This theorem is referenced by:  sbcom  2165  sbcomOLD  2166  sbcom2  2191  r19.12sn  3873  ordsucelsuc  4803  ordsucsssuc  4804  fvopab3g  5803  fvimacnvALT  5850  respreima  5860  fmptco  5902  fnsuppres  5953  cocan1  6025  cocan2  6026  smoword  6629  oaword  6793  omword  6814  om00el  6820  oeword  6834  nnaword  6871  nnmword  6877  swoer  6934  erth  6950  brecop  6998  eceqoveq  7010  xpdom2  7204  pw2f1olem  7213  omsucdomOLD  7303  fisucdomOLD  7313  ixpfi2  7406  cantnfrescl  7633  rankr1bg  7730  r1pwcl  7774  fseqenlem1  7906  alephord3  7960  alephdom2  7969  engch  8504  fpwwe2lem7  8512  fpwwe2lem9  8514  ltexpi  8780  ltapi  8781  ltmpi  8782  ltsonq  8847  ltmnq  8850  1idpr  8907  addcanpr  8924  axpre-ltadd  9043  axlttri  9148  subsub23  9311  leadd1  9497  ltsub1  9525  ltsub2  9526  leord1  9555  eqord1  9556  lemul1  9863  lediv1  9876  lt2mul2div  9887  lerec  9893  lediv2  9901  le2msq  9911  suprleub  9973  infmrgelb  9989  ofsubeq0  9998  ofsubge0  10000  avgle1  10208  avgle2  10209  cnref1o  10608  xleneg  10805  xltadd1  10836  xsubge0  10841  xposdif  10842  xltmul1  10872  supxrleub  10906  infmxrgelb  10914  iooneg  11018  iccneg  11019  iccsplit  11030  iccshftr  11031  iccshftl  11033  iccdil  11035  icccntr  11037  fzsplit2  11077  fzaddel  11088  fzrev  11109  elfzo  11143  fzon  11159  elfzom1b  11192  negmod0  11257  leexp2  11435  ltexp2r  11437  cjreb  11929  sqrlt  12068  rexfiuz  12152  limsuplt  12274  o1lo1  12332  rlimresb  12360  lo1eq  12363  rlimeq  12364  o1eq  12365  isercoll  12462  efle  12720  tanaddlem  12768  nndivdvds  12859  moddvds  12860  oddm1even  12910  bitsp1  12944  sadcaddlem  12970  sadadd  12980  sadass  12984  bitsshft  12988  smuval2  12995  smumul  13006  dvdssq  13061  phiprmpw  13166  eulerthlem2  13172  odzdvds  13182  pc2dvds  13253  1arith  13296  imasleval  13767  mreacs  13884  catpropd  13936  oppcsect  14000  funcres2b  14095  fthsect  14123  fthinv  14124  fucsect  14170  fucinv  14171  latnlemlt  14514  latnle  14515  ipole  14585  ipolt  14586  spwex  14662  issubg3  14961  eqgid  14993  resghm2b  15025  conjghm  15037  gastacos  15088  resscntz  15131  cntzrec  15133  oppgsubm  15159  oppgsubg  15160  sylow3lem6  15267  lsmcom2  15290  lsmass  15303  lsmcomx  15472  subgdmdprd  15593  opprsubrg  15890  lsslss  16038  lbspropd  16172  islbs2  16227  rspsn  16326  psrbagconf1o  16440  gsumbagdiaglem  16441  mplmonmul  16528  prmirred  16776  znfld  16842  basdif0  17019  neiptopreu  17198  neitr  17245  restlp  17248  cnrest2  17351  cnprest  17354  cnprest2  17355  lmss  17363  lmff  17366  ist1-2  17412  lpcls  17429  perfcls  17430  cmpfi  17472  hauseqlcld  17679  txlm  17681  txkgen  17685  xkopt  17688  idqtop  17739  tgqtop  17745  qtopcn  17747  uffix  17954  fmco  17994  flimrest  18016  lmflf  18038  txflf  18039  fclsrest  18057  cnpfcf  18074  tsmsgsum  18169  tsmsres  18174  tsmsf1o  18175  fmucndlem  18322  ismet2  18364  imasf1oxmet  18406  blres  18462  xmetec  18465  imasf1obl  18519  imasf1oxms  18520  prdsbl  18522  stdbdbl  18548  metrest  18555  metustsymOLD  18592  metustsym  18593  blval2  18606  metuel2  18610  tngngp  18696  cnbl0  18809  cnblcld  18810  bl2ioo  18824  cncfcnvcn  18952  iihalf2  18959  icoopnst  18965  iocopnst  18966  icopnfcnv  18968  icopnfhmeo  18969  cphorthcom  19164  caucfil  19237  lmclim  19256  cmsss  19304  volsup  19451  dyaddisjlem  19488  mbfeqalem  19535  mbfeqa  19536  mbfmulc2lem  19540  mbfmax  19542  mbfposr  19545  ismbf3d  19547  mbfimaopnlem  19548  mbfaddlem  19553  mbfsup  19557  mbfinf  19558  0plef  19565  0pledm  19566  i1fmulclem  19595  i1fres  19598  i1fpos  19599  itg1climres  19607  mbfi1fseqlem4  19611  itg2mulclem  19639  itg2monolem1  19643  itg2cnlem1  19654  iblre  19686  iblcn  19691  itgeqa  19706  ellimc2  19765  limcflf  19769  dvreslem  19797  lhop1  19899  ply1remlem  20086  fta1glem2  20090  ofmulrt  20200  plydiveu  20216  plyremlem  20222  quotcan  20227  ulmres  20305  cos11  20436  logleb  20499  argrege0  20507  logdivle  20518  efopn  20550  logccv  20555  cxplt  20586  cxple  20587  cxple2  20589  cxplt2  20590  cxplt3  20592  cxple3  20593  angrtmuld  20651  quad2  20680  atans2  20772  rlimcnp  20805  rlimcnp2  20806  rlimcxp  20813  sqff1o  20966  fsumvma2  20999  dchrptlem2  21050  lgsdilem  21107  lgsne0  21118  lgsqr  21131  lgsquadlem1  21139  lgsquadlem2  21140  m1lgs  21147  dchrisum0lem1  21211  padicabv  21325  uhgraeq12d  21343  usgraeq12d  21386  nbgrasym  21450  cusgrauvtxb  21506  eupath2lem3  21702  rngosn3  22015  nvsubsub23  22144  nmorepnf  22270  blocnilem  22306  ubthlem1  22373  shscom  22822  pjpreeq  22901  spansncol  23071  cmcm2  23119  hodsi  23279  nmoprepnf  23371  nmfnrepnf  23384  pjssposi  23676  cvcon3  23788  mdsymlem8  23914  dmdsym  23917  unipreima  24057  fmptcof2  24077  1stpreima  24096  metider  24290  pstmxmet  24293  xrge0iifiso  24322  logblt  24407  indpi1  24420  indf1ofs  24424  aean  24596  brfae  24600  subfacp1lem3  24869  subfacp1lem5  24871  opelco3  25404  predfz  25479  sscoid  25759  colinearalglem2  25847  axcgrid  25856  cgrcomr  25932  ofscom  25942  cgr3permute3  25982  cgr3permute1  25983  cgr3com  25988  colinearperm1  25997  colinearperm3  25998  outsideofcom  26063  itg2addnclem2  26258  ftc1anclem1  26281  ftc1anclem5  26285  ftc1anclem6  26286  areacirclem5  26297  areacirc  26298  opnbnd  26329  filnetlem4  26411  caures  26467  cnpwstotbnd  26507  ismtyima  26513  rrnmet  26539  reheibor  26549  fnnfpeq0  26740  lzenom  26829  rmxycomplete  26981  fzneg  27048  modabsdifz  27057  jm2.19  27065  pw2f1ocnv  27109  lindfmm  27275  lindsmm  27276  lsslindf  27278  lsslinds  27279  islindf4  27286  caofcan  27518  rfcnpre1  27667  rfcnpre2  27679  pr1eqbg  28057  usg2wlkeq  28305  usg2spot2nb  28455  sbcomwAUX7  29589  sbcom2NEW7  29645  ax7w15lemAUX7  29668  ax7w15AUX7  29669  ax7w14AUX7  29671  sbcomOLD7  29756  lcvbr  29820  lkrsc  29896  lshpkrlem1  29909  opltcon3b  30003  cmt2N  30049  cmt3N  30050  cvrcon3b  30076  cvrcmp2  30083  cvlexchb2  30130  cvlatexchb2  30134  2llnmj  30358  4atlem3  30394  4atlem9  30401  4atlem10a  30402  4atlem11a  30405  4atlem12a  30408  4at2  30412  2lplnmj  30420  llnexchb2  30667  lautlt  30889  lautcvr  30890  lautco  30895  ltrnatb  30935  ltrneq2  30946  cdlemefrs29pre00  31193  cdlemefrs29cpre1  31196  cdleme32fva  31235  dibglbN  31965  dochsncom  32181  dochkrsat  32254  lspindp5  32569  mapdh8ab  32576  hdmapip0com  32719
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 179
  Copyright terms: Public domain W3C validator