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  2166  sbcomOLD  2167  sbcom2  2192  r19.12sn  3874  ordsucelsuc  4804  ordsucsssuc  4805  fvopab3g  5804  fvimacnvALT  5851  respreima  5861  fmptco  5903  fnsuppres  5954  cocan1  6026  cocan2  6027  smoword  6630  oaword  6794  omword  6815  om00el  6821  oeword  6835  nnaword  6872  nnmword  6878  swoer  6935  erth  6951  brecop  6999  eceqoveq  7011  xpdom2  7205  pw2f1olem  7214  omsucdomOLD  7304  fisucdomOLD  7314  ixpfi2  7407  cantnfrescl  7634  rankr1bg  7731  r1pwcl  7775  fseqenlem1  7907  alephord3  7961  alephdom2  7970  engch  8505  fpwwe2lem7  8513  fpwwe2lem9  8515  ltexpi  8781  ltapi  8782  ltmpi  8783  ltsonq  8848  ltmnq  8851  1idpr  8908  addcanpr  8925  axpre-ltadd  9044  axlttri  9149  subsub23  9312  leadd1  9498  ltsub1  9526  ltsub2  9527  leord1  9556  eqord1  9557  lemul1  9864  lediv1  9877  lt2mul2div  9888  lerec  9894  lediv2  9902  le2msq  9912  suprleub  9974  infmrgelb  9990  ofsubeq0  9999  ofsubge0  10001  avgle1  10209  avgle2  10210  cnref1o  10609  xleneg  10806  xltadd1  10837  xsubge0  10842  xposdif  10843  xltmul1  10873  supxrleub  10907  infmxrgelb  10915  iooneg  11019  iccneg  11020  iccsplit  11031  iccshftr  11032  iccshftl  11034  iccdil  11036  icccntr  11038  fzsplit2  11078  fzaddel  11089  fzrev  11110  elfzo  11144  fzon  11160  elfzom1b  11193  negmod0  11258  leexp2  11436  ltexp2r  11438  cjreb  11930  sqrlt  12069  rexfiuz  12153  limsuplt  12275  o1lo1  12333  rlimresb  12361  lo1eq  12364  rlimeq  12365  o1eq  12366  isercoll  12463  efle  12721  tanaddlem  12769  nndivdvds  12860  moddvds  12861  oddm1even  12911  bitsp1  12945  sadcaddlem  12971  sadadd  12981  sadass  12985  bitsshft  12989  smuval2  12996  smumul  13007  dvdssq  13062  phiprmpw  13167  eulerthlem2  13173  odzdvds  13183  pc2dvds  13254  1arith  13297  imasleval  13768  mreacs  13885  catpropd  13937  oppcsect  14001  funcres2b  14096  fthsect  14124  fthinv  14125  fucsect  14171  fucinv  14172  latnlemlt  14515  latnle  14516  ipole  14586  ipolt  14587  spwex  14663  issubg3  14962  eqgid  14994  resghm2b  15026  conjghm  15038  gastacos  15089  resscntz  15132  cntzrec  15134  oppgsubm  15160  oppgsubg  15161  sylow3lem6  15268  lsmcom2  15291  lsmass  15304  lsmcomx  15473  subgdmdprd  15594  opprsubrg  15891  lsslss  16039  lbspropd  16173  islbs2  16228  rspsn  16327  psrbagconf1o  16441  gsumbagdiaglem  16442  mplmonmul  16529  prmirred  16777  znfld  16843  basdif0  17020  neiptopreu  17199  neitr  17246  restlp  17249  cnrest2  17352  cnprest  17355  cnprest2  17356  lmss  17364  lmff  17367  ist1-2  17413  lpcls  17430  perfcls  17431  cmpfi  17473  hauseqlcld  17680  txlm  17682  txkgen  17686  xkopt  17689  idqtop  17740  tgqtop  17746  qtopcn  17748  uffix  17955  fmco  17995  flimrest  18017  lmflf  18039  txflf  18040  fclsrest  18058  cnpfcf  18075  tsmsgsum  18170  tsmsres  18175  tsmsf1o  18176  fmucndlem  18323  ismet2  18365  imasf1oxmet  18407  blres  18463  xmetec  18466  imasf1obl  18520  imasf1oxms  18521  prdsbl  18523  stdbdbl  18549  metrest  18556  metustsymOLD  18593  metustsym  18594  blval2  18607  metuel2  18611  tngngp  18697  cnbl0  18810  cnblcld  18811  bl2ioo  18825  cncfcnvcn  18953  iihalf2  18960  icoopnst  18966  iocopnst  18967  icopnfcnv  18969  icopnfhmeo  18970  cphorthcom  19165  caucfil  19238  lmclim  19257  cmsss  19305  volsup  19452  dyaddisjlem  19489  mbfeqalem  19536  mbfeqa  19537  mbfmulc2lem  19541  mbfmax  19543  mbfposr  19546  ismbf3d  19548  mbfimaopnlem  19549  mbfaddlem  19554  mbfsup  19558  mbfinf  19559  0plef  19566  0pledm  19567  i1fmulclem  19596  i1fres  19599  i1fpos  19600  itg1climres  19608  mbfi1fseqlem4  19612  itg2mulclem  19640  itg2monolem1  19644  itg2cnlem1  19655  iblre  19687  iblcn  19692  itgeqa  19707  ellimc2  19766  limcflf  19770  dvreslem  19798  lhop1  19900  ply1remlem  20087  fta1glem2  20091  ofmulrt  20201  plydiveu  20217  plyremlem  20223  quotcan  20228  ulmres  20306  cos11  20437  logleb  20500  argrege0  20508  logdivle  20519  efopn  20551  logccv  20556  cxplt  20587  cxple  20588  cxple2  20590  cxplt2  20591  cxplt3  20593  cxple3  20594  angrtmuld  20652  quad2  20681  atans2  20773  rlimcnp  20806  rlimcnp2  20807  rlimcxp  20814  sqff1o  20967  fsumvma2  21000  dchrptlem2  21051  lgsdilem  21108  lgsne0  21119  lgsqr  21132  lgsquadlem1  21140  lgsquadlem2  21141  m1lgs  21148  dchrisum0lem1  21212  padicabv  21326  uhgraeq12d  21344  usgraeq12d  21387  nbgrasym  21451  cusgrauvtxb  21507  eupath2lem3  21703  rngosn3  22016  nvsubsub23  22145  nmorepnf  22271  blocnilem  22307  ubthlem1  22374  shscom  22823  pjpreeq  22902  spansncol  23072  cmcm2  23120  hodsi  23280  nmoprepnf  23372  nmfnrepnf  23385  pjssposi  23677  cvcon3  23789  mdsymlem8  23915  dmdsym  23918  unipreima  24058  fmptcof2  24078  1stpreima  24097  metider  24291  pstmxmet  24294  xrge0iifiso  24323  logblt  24408  indpi1  24421  indf1ofs  24425  aean  24597  brfae  24601  subfacp1lem3  24870  subfacp1lem5  24872  opelco3  25405  predfz  25480  sscoid  25760  colinearalglem2  25848  axcgrid  25857  cgrcomr  25933  ofscom  25943  cgr3permute3  25983  cgr3permute1  25984  cgr3com  25989  colinearperm1  25998  colinearperm3  25999  outsideofcom  26064  itg2addnclem2  26259  ftc1anclem1  26282  ftc1anclem5  26286  ftc1anclem6  26287  areacirclem5  26298  areacirc  26299  opnbnd  26330  filnetlem4  26412  caures  26468  cnpwstotbnd  26508  ismtyima  26514  rrnmet  26540  reheibor  26550  fnnfpeq0  26741  lzenom  26830  rmxycomplete  26982  fzneg  27049  modabsdifz  27058  jm2.19  27066  pw2f1ocnv  27110  lindfmm  27276  lindsmm  27277  lsslindf  27279  lsslinds  27280  islindf4  27287  caofcan  27519  rfcnpre1  27668  rfcnpre2  27680  pr1eqbg  28058  usg2wlkeq  28330  usg2spot2nb  28516  sbcomwAUX7  29650  sbcom2NEW7  29706  ax7w15lemAUX7  29729  ax7w15AUX7  29730  ax7w14AUX7  29732  sbcomOLD7  29817  lcvbr  29881  lkrsc  29957  lshpkrlem1  29970  opltcon3b  30064  cmt2N  30110  cmt3N  30111  cvrcon3b  30137  cvrcmp2  30144  cvlexchb2  30191  cvlatexchb2  30195  2llnmj  30419  4atlem3  30455  4atlem9  30462  4atlem10a  30463  4atlem11a  30466  4atlem12a  30469  4at2  30473  2lplnmj  30481  llnexchb2  30728  lautlt  30950  lautcvr  30951  lautco  30956  ltrnatb  30996  ltrneq2  31007  cdlemefrs29pre00  31254  cdlemefrs29cpre1  31257  cdleme32fva  31296  dibglbN  32026  dochsncom  32242  dochkrsat  32315  lspindp5  32630  mapdh8ab  32637  hdmapip0com  32780
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