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  4069  sbcbr  4478  fvopab3g  5960  fvimacnvALT  6016  respreima  6024  fmptco  6071  fnnfpeq0  6110  cocan1  6204  cocan2  6205  ordsucelsuc  6663  ordsucsssuc  6664  fnsuppres  6953  smoword  7093  oaword  7258  omword  7279  om00el  7285  oeword  7299  nnaword  7336  nnmword  7342  swoer  7399  erth  7416  brecop  7464  eceqoveq  7476  xpdom2  7673  pw2f1olem  7682  ixpfi2  7878  wemapso2lem  8067  cantnfrescl  8180  rankr1bg  8273  r1pwcl  8317  fseqenlem1  8453  alephord3  8507  alephdom2  8516  engch  9052  fpwwe2lem7  9060  fpwwe2lem9  9062  ltexpi  9326  ltapi  9327  ltmpi  9328  ltsonq  9393  ltmnq  9396  1idpr  9453  addcanpr  9470  axpre-ltadd  9590  axlttri  9704  subsub23  9879  leadd1  10081  ltsub1  10109  ltsub2  10110  leord1  10140  eqord1  10141  lemul1  10456  lediv1  10469  lt2mul2div  10482  lerec  10488  lediv2  10496  le2msq  10506  suprleub  10573  infregelb  10594  infmrgelbOLD  10595  ofsubeq0  10606  ofsubge0  10608  avgle1  10852  avgle2  10853  cnref1o  11297  xleneg  11511  xltadd1  11542  xsubge0  11547  xposdif  11548  xltmul1  11578  supxrleub  11612  infxrgelb  11621  infmxrgelbOLD  11625  iooneg  11750  iccneg  11751  iccsplit  11763  iccshftr  11764  iccshftl  11766  iccdil  11768  icccntr  11770  fzsplit2  11822  fzaddel  11831  fzrev  11856  predfz  11912  elfzo  11920  nelfzo  11923  fzon  11937  elfzom1b  12007  negmod0  12102  leexp2  12324  ltexp2r  12326  repswsymball  12867  repswsymballbi  12868  cjreb  13165  sqrtlt  13304  limsuplt  13516  limsupltOLD  13517  o1lo1  13579  rlimresb  13607  lo1eq  13610  rlimeq  13611  o1eq  13612  isercoll  13709  efle  14150  tanaddlem  14198  nndivdvds  14289  moddvds  14290  oddm1even  14344  bitsp1  14379  sadcaddlem  14405  sadadd  14415  sadass  14419  bitsshft  14423  smuval2  14430  smumul  14441  dvdssq  14499  phiprmpw  14684  eulerthlem2  14690  odzdvds  14700  pc2dvds  14782  1arith  14825  imasleval  15389  mreacs  15506  catpropd  15556  oppcsect  15625  funcres2b  15744  fthsect  15772  fthinv  15773  fucsect  15819  fucinv  15820  latnlemlt  16272  latnle  16273  ipole  16346  ipolt  16347  issubg3  16777  eqgid  16811  resghm2b  16843  conjghm  16855  gastacos  16906  resscntz  16927  cntzrec  16929  oppgsubm  16955  oppgsubg  16956  sylow3lem6  17210  lsmcom2  17233  lsmass  17246  lsmcomx  17420  subgdmdprd  17593  opprsubrg  17955  lsslss  18110  lbspropd  18248  islbs2  18303  rspsn  18404  psrbagconf1o  18524  gsumbagdiaglem  18525  mplmonmul  18614  prmirred  18988  znfld  19053  lindfmm  19307  lindsmm  19308  lsslindf  19310  lsslinds  19311  islindf4  19318  basdif0  19890  neiptopreu  20071  neitr  20118  restlp  20121  cnrest2  20224  cnprest  20227  cnprest2  20228  lmss  20236  lmff  20239  ist1-2  20285  lpcls  20302  perfcls  20303  cmpfi  20345  hauseqlcld  20583  txlm  20585  txkgen  20589  xkopt  20592  idqtop  20643  tgqtop  20649  qtopcn  20651  uffix  20858  fmco  20898  flimrest  20920  lmflf  20942  txflf  20943  fclsrest  20961  cnpfcf  20978  tsmsgsum  21075  tsmsres  21080  tsmsf1o  21081  fmucndlem  21228  ismet2  21270  imasf1oxmet  21312  blres  21368  xmetec  21371  imasf1obl  21425  imasf1oxms  21426  prdsbl  21428  stdbdbl  21454  metrest  21461  metustsym  21492  blval2  21499  metuel2  21502  tngngp  21584  cnbl0  21696  cnblcld  21697  bl2ioo  21712  cncfcnvcn  21840  iihalf2  21848  icoopnst  21854  iocopnst  21855  icopnfcnv  21857  icopnfhmeo  21858  cphorthcom  22062  caucfil  22137  lmclim  22156  cmsss  22202  rrxmet  22246  volsup  22377  dyaddisjlem  22421  mbfeqalem  22466  mbfeqa  22467  mbfmulc2lem  22471  mbfmax  22473  mbfposr  22476  ismbf3d  22478  mbfimaopnlem  22479  mbfaddlem  22484  mbfsup  22488  mbfinf  22489  mbfinfOLD  22490  0plef  22498  0pledm  22499  i1fmulclem  22528  i1fres  22531  i1fpos  22532  itg1climres  22540  mbfi1fseqlem4  22544  itg2mulclem  22572  itg2monolem1  22576  itg2cnlem1  22587  iblre  22619  iblcn  22624  itgeqa  22639  ellimc2  22700  limcflf  22704  dvreslem  22732  lhop1  22834  ply1remlem  22979  fta1glem2  22983  ofmulrt  23094  plydiveu  23110  plyremlem  23116  quotcan  23121  ulmres  23199  cos11  23338  logleb  23408  argrege0  23416  logdivle  23427  efopn  23459  logccv  23464  cxplt  23495  cxple  23496  cxple2  23498  cxplt2  23499  cxplt3  23501  cxple3  23502  logbleb  23576  logblt  23577  angrtmuld  23593  quad2  23621  atans2  23713  rlimcnp  23747  rlimcnp2  23748  rlimcxp  23755  sqff1o  23963  fsumvma2  23996  dchrptlem2  24047  lgsdilem  24104  lgsne0  24115  lgsqr  24128  lgsquadlem1  24136  lgsquadlem2  24137  m1lgs  24144  dchrisum0lem1  24208  padicabv  24322  trgcgrg  24413  colcom  24454  colrot1  24455  ishlg  24498  hlcomb  24499  hlbtwn  24507  lncom  24517  lnrot2  24519  israg  24590  perpcom  24606  hpgcom  24656  colopp  24658  iscgra  24698  isinag  24723  colinearalglem2  24774  axcgrid  24783  uhgraeq12d  24871  usgraeq12d  24926  nbgrasym  25003  cusgrauvtxb  25060  usg2wlkeq  25272  clwlkisclwwlk  25353  eupath2lem3  25543  usg2spot2nb  25629  rngosn3  25990  nvsubsub23  26119  nmorepnf  26245  blocnilem  26281  ubthlem1  26348  shscom  26798  pjpreeq  26877  spansncol  27047  cmcm2  27095  hodsi  27254  nmoprepnf  27346  nmfnrepnf  27359  pjssposi  27651  cvcon3  27763  mdsymlem8  27889  dmdsym  27892  disjunsn  28034  fimarab  28075  unipreima  28076  fmptcof2  28090  1stpreima  28118  fpwrelmapffslem  28151  infxrge0gelb  28178  nndiffz1  28193  isinftm  28327  metidv  28525  metider  28527  pstmxmet  28530  xrge0iifiso  28571  indpi1  28673  indf1ofs  28677  aean  28897  brfae  28901  signsply0  29219  signsvfn  29250  subfacp1lem3  29684  subfacp1lem5  29686  opelco3  30198  sscoid  30456  cgrcomr  30540  ofscom  30550  cgr3permute3  30590  cgr3permute1  30591  cgr3com  30596  colinearperm1  30605  colinearperm3  30606  outsideofcom  30671  opnbnd  30757  filnetlem4  30813  wl-equsald  31570  wl-sbcom3  31619  poimirlem23  31657  broucube  31668  heicant  31669  itg2addnclem2  31688  ftc1anclem1  31711  ftc1anclem5  31715  ftc1anclem6  31716  areacirclem5  31730  areacirc  31731  caures  31783  cnpwstotbnd  31823  ismtyima  31829  rrnmet  31855  reheibor  31865  lcvbr  32286  lkrsc  32362  lshpkrlem1  32375  opltcon3b  32469  cmt2N  32515  cmt3N  32516  cvrcon3b  32542  cvrcmp2  32549  cvlexchb2  32596  cvlatexchb2  32600  2llnmj  32824  4atlem3  32860  4atlem9  32867  4atlem10a  32868  4atlem11a  32871  4atlem12a  32874  4at2  32878  2lplnmj  32886  llnexchb2  33133  lautlt  33355  lautcvr  33356  lautco  33361  ltrnatb  33401  ltrneq2  33412  cdlemefrs29pre00  33661  cdlemefrs29cpre1  33664  cdleme32fva  33703  dibglbN  34433  dochsncom  34649  dochkrsat  34722  lspindp5  35037  mapdh8ab  35044  hdmapip0com  35187  lzenom  35311  rmxycomplete  35461  fzneg  35528  modabsdifz  35535  jm2.19  35544  pw2f1ocnv  35588  brtrclfv2  35948  caofcan  36299  rfcnpre1  36970  rfcnpre2  36982  ellimcabssub0  37259  fperdvper  37352  pr1eqbg  38364  isfusgracl  38486  isfusgraclALT  38488  fusgraimpclALT2  38491  mgmpropd  38523  lco0  38970  lindslininds  39007  ltsubaddb  39061  ltsubsubb  39062  ltsubadd2b  39063  elbigolo1  39119  dig2bits  39176