Theorem 3bitr4d 288

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

Step	Hyp	Ref	Expression
1		3bitr4d.2	. 2 |- ( ph -> ( th <-> ps ) )
2		3bitr4d.1	. . 3 |- ( ph -> ( ps <-> ch ) )
3		3bitr4d.3	. . 3 |- ( ph -> ( ta <-> ch ) )
4	2, 3	bitr4d 259	. 2 |- ( ph -> ( ps <-> ta ) )
5	1, 4	bitrd 256	1 |- ( ph -> ( th <-> ta ) )

Syntax hints:   -> wi 4   <-> wb 187

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 188

This theorem is referenced by:  r19.12snOLD  4066  sbcbr  4476  fvopab3g  5960  fvimacnvALT  6016  respreima  6024  fmptco  6071  fnnfpeq0  6110  cocan1  6204  cocan2  6205  ordsucelsuc  6663  ordsucsssuc  6664  fnsuppres  6953  smoword  7096  oaword  7261  omword  7282  om00el  7288  oeword  7302  nnaword  7339  nnmword  7345  swoer  7402  erth  7419  brecop  7467  eceqoveq  7479  xpdom2  7676  pw2f1olem  7685  ixpfi2  7881  wemapso2lem  8076  cantnfrescl  8189  rankr1bg  8282  r1pwcl  8326  fseqenlem1  8462  alephord3  8516  alephdom2  8525  engch  9060  fpwwe2lem7  9068  fpwwe2lem9  9070  ltexpi  9334  ltapi  9335  ltmpi  9336  ltsonq  9401  ltmnq  9404  1idpr  9461  addcanpr  9478  axpre-ltadd  9598  axlttri  9712  subsub23  9887  leadd1  10089  ltsub1  10117  ltsub2  10118  leord1  10148  eqord1  10149  lemul1  10464  lediv1  10477  lt2mul2div  10490  lerec  10496  lediv2  10503  le2msq  10513  suprleub  10580  infregelb  10601  infmrgelbOLD  10602  ofsubeq0  10613  ofsubge0  10615  avgle1  10859  avgle2  10860  cnref1o  11304  xleneg  11518  xltadd1  11549  xsubge0  11554  xposdif  11555  xltmul1  11585  supxrleub  11619  infxrgelb  11628  infmxrgelbOLD  11632  iooneg  11759  iccneg  11760  iccsplit  11772  iccshftr  11773  iccshftl  11775  iccdil  11777  icccntr  11779  fzsplit2  11831  fzaddel  11840  fzrev  11865  predfz  11921  elfzo  11929  nelfzo  11932  fzon  11946  elfzom1b  12016  negmod0  12111  leexp2  12333  ltexp2r  12335  repswsymball  12884  repswsymballbi  12885  cjreb  13186  sqrtlt  13325  limsuplt  13537  limsupltOLD  13538  o1lo1  13600  rlimresb  13628  lo1eq  13631  rlimeq  13632  o1eq  13633  isercoll  13730  efle  14171  tanaddlem  14219  nndivdvds  14310  moddvds  14311  oddm1even  14365  bitsp1  14403  sadcaddlem  14430  sadadd  14440  sadass  14444  bitsshft  14448  smuval2  14455  smumul  14466  dvdssq  14527  phiprmpw  14723  eulerthlem2  14729  odzdvds  14739  odzdvdsOLD  14745  pc2dvds  14827  1arith  14870  imasleval  15446  mreacs  15563  catpropd  15613  oppcsect  15682  funcres2b  15801  fthsect  15829  fthinv  15830  fucsect  15876  fucinv  15877  latnlemlt  16329  latnle  16330  ipole  16403  ipolt  16404  issubg3  16834  eqgid  16868  resghm2b  16900  conjghm  16912  gastacos  16963  resscntz  16984  cntzrec  16986  oppgsubm  17012  oppgsubg  17013  sylow3lem6  17283  lsmcom2  17306  lsmass  17319  lsmcomx  17493  subgdmdprd  17666  opprsubrg  18028  lsslss  18183  lbspropd  18321  islbs2  18376  rspsn  18477  psrbagconf1o  18597  gsumbagdiaglem  18598  mplmonmul  18687  prmirred  19064  znfld  19129  lindfmm  19383  lindsmm  19384  lsslindf  19386  lsslinds  19387  islindf4  19394  basdif0  19966  neiptopreu  20147  neitr  20194  restlp  20197  cnrest2  20300  cnprest  20303  cnprest2  20304  lmss  20312  lmff  20315  ist1-2  20361  lpcls  20378  perfcls  20379  cmpfi  20421  hauseqlcld  20659  txlm  20661  txkgen  20665  xkopt  20668  idqtop  20719  tgqtop  20725  qtopcn  20727  uffix  20934  fmco  20974  flimrest  20996  lmflf  21018  txflf  21019  fclsrest  21037  cnpfcf  21054  tsmsgsum  21151  tsmsres  21156  tsmsf1o  21157  fmucndlem  21304  ismet2  21346  imasf1oxmet  21388  blres  21444  xmetec  21447  imasf1obl  21501  imasf1oxms  21502  prdsbl  21504  stdbdbl  21530  metrest  21537  metustsym  21568  blval2  21575  metuel2  21578  tngngp  21660  cnbl0  21792  cnblcld  21793  bl2ioo  21808  cncfcnvcn  21951  iihalf2  21959  icoopnst  21965  iocopnst  21966  icopnfcnv  21968  icopnfhmeo  21969  cphorthcom  22176  caucfil  22251  lmclim  22270  cmsss  22316  rrxmet  22360  volsup  22507  dyaddisjlem  22551  mbfeqalem  22596  mbfeqa  22597  mbfmulc2lem  22601  mbfmax  22603  mbfposr  22606  ismbf3d  22608  mbfimaopnlem  22609  mbfaddlem  22614  mbfsup  22618  mbfinf  22619  mbfinfOLD  22620  0plef  22628  0pledm  22629  i1fmulclem  22658  i1fres  22661  i1fpos  22662  itg1climres  22670  mbfi1fseqlem4  22674  itg2mulclem  22702  itg2monolem1  22706  itg2cnlem1  22717  iblre  22749  iblcn  22754  itgeqa  22769  ellimc2  22830  limcflf  22834  dvreslem  22862  lhop1  22964  ply1remlem  23111  fta1glem2  23115  ofmulrt  23233  plydiveu  23249  plyremlem  23255  quotcan  23260  ulmres  23341  cos11  23480  logleb  23550  argrege0  23558  logdivle  23569  efopn  23601  logccv  23606  cxplt  23637  cxple  23638  cxple2  23640  cxplt2  23641  cxplt3  23643  cxple3  23644  logbleb  23718  logblt  23719  angrtmuld  23735  quad2  23763  atans2  23855  rlimcnp  23889  rlimcnp2  23890  rlimcxp  23897  sqff1o  24107  fsumvma2  24140  dchrptlem2  24191  lgsdilem  24248  lgsne0  24259  lgsqr  24272  lgsquadlem1  24280  lgsquadlem2  24281  m1lgs  24288  dchrisum0lem1  24352  padicabv  24466  trgcgrg  24558  colcom  24601  colrot1  24602  ishlg  24645  hlcomb  24646  hlbtwn  24654  lncom  24665  lnrot2  24667  israg  24740  perpcom  24756  hpgcom  24807  colopp  24809  iscgra  24849  isinag  24877  colinearalglem2  24935  axcgrid  24944  uhgraeq12d  25032  usgraeq12d  25087  nbgrasym  25165  cusgrauvtxb  25222  usg2wlkeq  25434  clwlkisclwwlk  25515  eupath2lem3  25705  usg2spot2nb  25791  rngosn3  26152  nvsubsub23  26281  nmorepnf  26407  blocnilem  26443  ubthlem1  26510  shscom  26970  pjpreeq  27049  spansncol  27219  cmcm2  27267  hodsi  27426  nmoprepnf  27518  nmfnrepnf  27531  pjssposi  27823  cvcon3  27935  mdsymlem8  28061  dmdsym  28064  disjunsn  28206  fimarab  28246  unipreima  28247  fmptcof2  28261  1stpreima  28289  fpwrelmapffslem  28323  infxrge0gelb  28356  infxrge0gelbOLD  28357  nndiffz1  28372  isinftm  28505  metidv  28703  metider  28705  pstmxmet  28708  xrge0iifiso  28749  indpi1  28851  indf1ofs  28855  aean  29075  brfae  29079  signsply0  29448  signsvfn  29479  subfacp1lem3  29913  subfacp1lem5  29915  opelco3  30427  sscoid  30685  cgrcomr  30769  ofscom  30779  cgr3permute3  30819  cgr3permute1  30820  cgr3com  30825  colinearperm1  30834  colinearperm3  30835  outsideofcom  30900  opnbnd  30986  filnetlem4  31042  finxpsuclem  31753  wl-equsald  31836  wl-sbcom3  31889  poimirlem23  31927  broucube  31938  heicant  31939  itg2addnclem2  31958  ftc1anclem1  31981  ftc1anclem5  31985  ftc1anclem6  31986  areacirclem5  32000  areacirc  32001  caures  32053  cnpwstotbnd  32093  ismtyima  32099  rrnmet  32125  reheibor  32135  lcvbr  32556  lkrsc  32632  lshpkrlem1  32645  opltcon3b  32739  cmt2N  32785  cmt3N  32786  cvrcon3b  32812  cvrcmp2  32819  cvlexchb2  32866  cvlatexchb2  32870  2llnmj  33094  4atlem3  33130  4atlem9  33137  4atlem10a  33138  4atlem11a  33141  4atlem12a  33144  4at2  33148  2lplnmj  33156  llnexchb2  33403  lautlt  33625  lautcvr  33626  lautco  33631  ltrnatb  33671  ltrneq2  33682  cdlemefrs29pre00  33931  cdlemefrs29cpre1  33934  cdleme32fva  33973  dibglbN  34703  dochsncom  34919  dochkrsat  34992  lspindp5  35307  mapdh8ab  35314  hdmapip0com  35457  lzenom  35581  rmxycomplete  35735  fzneg  35802  modabsdifz  35809  jm2.19  35818  pw2f1ocnv  35862  brtrclfv2  36289  caofcan  36642  rfcnpre1  37313  rfcnpre2  37325  ellimcabssub0  37637  fperdvper  37730  pr1eqbg  38857  nbgrsym  39201  uvtxa01vtx0  39227  iscplgredg  39241  isfusgracl  39357  isfusgraclALT  39359  fusgraimpclALT2  39362  mgmpropd  39394  lco0  39841  lindslininds  39878  ltsubaddb  39932  ltsubsubb  39933  ltsubadd2b  39934  elbigolo1  39989  dig2bits  40046