Theorem 3bitr4d 285

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 256	. 2 |- ( ph -> ( ps <-> ta ) )
5	1, 4	bitrd 253	1 |- ( ph -> ( th <-> ta ) )

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

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 185

This theorem is referenced by:  sbcomOLD  2118  sbcom2OLD  2154  r19.12sn  3929  sbcbr  4333  fvopab3g  5758  fvimacnvALT  5810  respreima  5820  fmptco  5863  fnnfpeq0  5896  fnsuppresOLD  5925  cocan1  5982  cocan2  5983  ordsucelsuc  6422  ordsucsssuc  6423  fnsuppres  6705  smoword  6813  oaword  6976  omword  6997  om00el  7003  oeword  7017  nnaword  7054  nnmword  7060  swoer  7117  erth  7133  brecop  7181  eceqoveq  7193  xpdom2  7394  pw2f1olem  7403  omsucdomOLD  7494  fisucdomOLD  7504  ixpfi2  7597  wemapso2lem  7755  cantnfrescl  7872  rankr1bg  7998  r1pwcl  8042  fseqenlem1  8182  alephord3  8236  alephdom2  8245  engch  8783  fpwwe2lem7  8791  fpwwe2lem9  8793  ltexpi  9059  ltapi  9060  ltmpi  9061  ltsonq  9126  ltmnq  9129  1idpr  9186  addcanpr  9203  axpre-ltadd  9322  axlttri  9434  subsub23  9603  leadd1  9795  ltsub1  9823  ltsub2  9824  leord1  9855  eqord1  9856  lemul1  10169  lediv1  10182  lt2mul2div  10196  lerec  10202  lediv2  10210  le2msq  10220  suprleub  10282  infmrgelb  10298  ofsubeq0  10307  ofsubge0  10309  avgle1  10552  avgle2  10553  cnref1o  10974  xleneg  11176  xltadd1  11207  xsubge0  11212  xposdif  11213  xltmul1  11243  supxrleub  11277  infmxrgelb  11285  iooneg  11392  iccneg  11393  iccsplit  11405  iccshftr  11406  iccshftl  11408  iccdil  11410  icccntr  11412  fzsplit2  11461  fzaddel  11480  fzrev  11503  elfzo  11539  fzon  11555  elfzom1b  11610  negmod0  11700  leexp2  11902  ltexp2r  11904  repswsymball  12401  repswsymballbi  12402  cjreb  12596  sqrlt  12735  limsuplt  12941  o1lo1  12999  rlimresb  13027  lo1eq  13030  rlimeq  13031  o1eq  13032  isercoll  13129  efle  13385  tanaddlem  13433  nndivdvds  13524  moddvds  13525  oddm1even  13576  bitsp1  13610  sadcaddlem  13636  sadadd  13646  sadass  13650  bitsshft  13654  smuval2  13661  smumul  13672  dvdssq  13727  phiprmpw  13834  eulerthlem2  13840  odzdvds  13850  pc2dvds  13928  1arith  13971  imasleval  14462  mreacs  14579  catpropd  14631  oppcsect  14695  funcres2b  14790  fthsect  14818  fthinv  14819  fucsect  14865  fucinv  14866  latnlemlt  15237  latnle  15238  ipole  15311  ipolt  15312  issubg3  15679  eqgid  15713  resghm2b  15745  conjghm  15757  gastacos  15808  resscntz  15829  cntzrec  15831  oppgsubm  15857  oppgsubg  15858  sylow3lem6  16111  lsmcom2  16134  lsmass  16147  lsmcomx  16318  subgdmdprd  16505  opprsubrg  16810  lsslss  16964  lbspropd  17102  islbs2  17157  rspsn  17258  psrbagconf1o  17378  gsumbagdiaglem  17379  mplmonmul  17477  prmirred  17761  prmirredOLD  17764  znfld  17835  lindfmm  18098  lindsmm  18099  lsslindf  18101  lsslinds  18102  islindf4  18109  basdif0  18400  neiptopreu  18579  neitr  18626  restlp  18629  cnrest2  18732  cnprest  18735  cnprest2  18736  lmss  18744  lmff  18747  ist1-2  18793  lpcls  18810  perfcls  18811  cmpfi  18853  hauseqlcld  19061  txlm  19063  txkgen  19067  xkopt  19070  idqtop  19121  tgqtop  19127  qtopcn  19129  uffix  19336  fmco  19376  flimrest  19398  lmflf  19420  txflf  19421  fclsrest  19439  cnpfcf  19456  tsmsgsum  19551  tsmsgsumOLD  19554  tsmsresOLD  19559  tsmsres  19560  tsmsf1o  19561  fmucndlem  19708  ismet2  19750  imasf1oxmet  19792  blres  19848  xmetec  19851  imasf1obl  19905  imasf1oxms  19906  prdsbl  19908  stdbdbl  19934  metrest  19941  metustsymOLD  19978  metustsym  19979  blval2  19992  metuel2  19996  tngngp  20082  cnbl0  20195  cnblcld  20196  bl2ioo  20211  cncfcnvcn  20339  iihalf2  20347  icoopnst  20353  iocopnst  20354  icopnfcnv  20356  icopnfhmeo  20357  cphorthcom  20561  caucfil  20636  lmclim  20655  cmsss  20703  rrxmet  20749  volsup  20879  dyaddisjlem  20917  mbfeqalem  20962  mbfeqa  20963  mbfmulc2lem  20967  mbfmax  20969  mbfposr  20972  ismbf3d  20974  mbfimaopnlem  20975  mbfaddlem  20980  mbfsup  20984  mbfinf  20985  0plef  20992  0pledm  20993  i1fmulclem  21022  i1fres  21025  i1fpos  21026  itg1climres  21034  mbfi1fseqlem4  21038  itg2mulclem  21066  itg2monolem1  21070  itg2cnlem1  21081  iblre  21113  iblcn  21118  itgeqa  21133  ellimc2  21194  limcflf  21198  dvreslem  21226  lhop1  21328  ply1remlem  21519  fta1glem2  21523  ofmulrt  21633  plydiveu  21649  plyremlem  21655  quotcan  21660  ulmres  21738  cos11  21874  logleb  21937  argrege0  21945  logdivle  21956  efopn  21988  logccv  21993  cxplt  22024  cxple  22025  cxple2  22027  cxplt2  22028  cxplt3  22030  cxple3  22031  angrtmuld  22089  quad2  22119  atans2  22211  rlimcnp  22244  rlimcnp2  22245  rlimcxp  22252  sqff1o  22405  fsumvma2  22438  dchrptlem2  22489  lgsdilem  22546  lgsne0  22557  lgsqr  22570  lgsquadlem1  22578  lgsquadlem2  22579  m1lgs  22586  dchrisum0lem1  22650  padicabv  22764  trgcgrg  22848  colcom  22871  colrot1  22872  lncom  22903  lnrot2  22905  colinearalglem2  22976  axcgrid  22985  uhgraeq12d  23064  usgraeq12d  23107  nbgrasym  23171  cusgrauvtxb  23227  eupath2lem3  23423  rngosn3  23736  nvsubsub23  23865  nmorepnf  23991  blocnilem  24027  ubthlem1  24094  shscom  24545  pjpreeq  24624  spansncol  24794  cmcm2  24842  hodsi  25002  nmoprepnf  25094  nmfnrepnf  25107  pjssposi  25399  cvcon3  25511  mdsymlem8  25637  dmdsym  25640  disjunsn  25760  unipreima  25785  fmptcof2  25803  1stpreima  25825  fpwrelmapffslem  25857  nndiffz1  25898  metider  26175  pstmxmet  26178  xrge0iifiso  26219  logblt  26319  indpi1  26332  indf1ofs  26336  aean  26514  brfae  26518  signsply0  26800  signsvfn  26831  subfacp1lem3  26918  subfacp1lem5  26920  opelco3  27436  predfz  27511  sscoid  27791  cgrcomr  27875  ofscom  27885  cgr3permute3  27925  cgr3permute1  27926  cgr3com  27931  colinearperm1  27940  colinearperm3  27941  outsideofcom  28006  wl-equsald  28216  wl-sbcom3  28255  heicant  28270  itg2addnclem2  28288  ftc1anclem1  28311  ftc1anclem5  28315  ftc1anclem6  28316  areacirclem5  28332  areacirc  28333  opnbnd  28364  filnetlem4  28446  caures  28500  cnpwstotbnd  28540  ismtyima  28546  rrnmet  28572  reheibor  28582  lzenom  28953  rmxycomplete  29103  fzneg  29170  modabsdifz  29179  jm2.19  29187  pw2f1ocnv  29231  caofcan  29442  rfcnpre1  29586  rfcnpre2  29598  pr1eqbg  29967  usg2wlkeq  30135  clwlkisclwwlk  30297  usg2spot2nb  30504  lco0  30691  lindslininds  30728  lcvbr  32260  lkrsc  32336  lshpkrlem1  32349  opltcon3b  32443  cmt2N  32489  cmt3N  32490  cvrcon3b  32516  cvrcmp2  32523  cvlexchb2  32570  cvlatexchb2  32574  2llnmj  32798  4atlem3  32834  4atlem9  32841  4atlem10a  32842  4atlem11a  32845  4atlem12a  32848  4at2  32852  2lplnmj  32860  llnexchb2  33107  lautlt  33329  lautcvr  33330  lautco  33335  ltrnatb  33375  ltrneq2  33386  cdlemefrs29pre00  33633  cdlemefrs29cpre1  33636  cdleme32fva  33675  dibglbN  34405  dochsncom  34621  dochkrsat  34694  lspindp5  35009  mapdh8ab  35016  hdmapip0com  35159