Theorem 3bitr4d 300

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

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

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 197

This theorem is referenced by:  pr1eqbg  4390  fvopab3g  6277  fvimacnvALT  6336  respreima  6344  fmptco  6396  fnnfpeq0  6444  cocan1  6546  cocan2  6547  ordsucelsuc  7022  ordsucsssuc  7023  fnsuppres  7322  smoword  7463  oaword  7629  omword  7650  om00el  7656  oeword  7670  nnaword  7707  nnmword  7713  swoer  7772  erth  7791  brecop  7840  eceqoveq  7853  xpdom2  8055  pw2f1olem  8064  ixpfi2  8264  wemapso2lem  8457  cantnfrescl  8573  rankr1bg  8666  r1pwcl  8710  fseqenlem1  8847  alephord3  8901  alephdom2  8910  engch  9450  fpwwe2lem7  9458  fpwwe2lem9  9460  ltexpi  9724  ltapi  9725  ltmpi  9726  ltsonq  9791  ltmnq  9794  1idpr  9851  addcanpr  9868  axpre-ltadd  9988  axlttri  10109  subsub23  10286  leadd1  10496  ltsub1  10524  ltsub2  10525  leord1  10555  eqord1  10556  lemul1  10875  lediv1  10888  lt2mul2div  10901  lerec  10906  lediv2  10913  le2msq  10923  suprleub  10989  infregelb  11007  ofsubeq0  11017  ofsubge0  11019  avgle1  11272  avgle2  11273  cnref1o  11827  xleneg  12049  xltadd1  12086  xsubge0  12091  xposdif  12092  xltmul1  12122  supxrleub  12156  infxrgelb  12165  iooneg  12292  iccneg  12293  iccsplit  12305  iccshftr  12306  iccshftl  12308  iccdil  12310  icccntr  12312  fzsplit2  12366  fzaddel  12375  fzrev  12403  predfz  12464  elfzo  12472  nelfzo  12475  fzon  12489  elfzom1b  12567  negmod0  12677  leexp2  12915  ltexp2r  12917  repswsymball  13526  repswsymballbi  13527  cjreb  13863  sqrtlt  14002  limsuplt  14210  o1lo1  14268  rlimresb  14296  lo1eq  14299  rlimeq  14300  o1eq  14301  isercoll  14398  efle  14848  tanaddlem  14896  nndivdvds  14989  moddvds  14991  modmulconst  15013  oddm1even  15067  ltoddhalfle  15085  bitsp1  15153  sadcaddlem  15179  sadadd  15189  sadass  15193  bitsshft  15197  smuval2  15204  smumul  15215  dvdssq  15280  phiprmpw  15481  eulerthlem2  15487  odzdvds  15500  pc2dvds  15583  1arith  15631  imasleval  16201  mreacs  16319  catpropd  16369  oppcsect  16438  funcres2b  16557  fthsect  16585  fthinv  16586  fucsect  16632  fucinv  16633  latnlemlt  17084  latnle  17085  ipole  17158  ipolt  17159  issubg3  17612  eqgid  17646  resghm2b  17678  conjghm  17691  gastacos  17743  resscntz  17764  cntzrec  17766  oppgsubm  17792  oppgsubg  17793  sylow3lem6  18047  lsmcom2  18070  lsmass  18083  ablsubsub23  18230  lsmcomx  18259  subgdmdprd  18433  opprsubrg  18801  lsslss  18961  lbspropd  19099  islbs2  19154  rspsn  19254  psrbagconf1o  19374  gsumbagdiaglem  19375  mplmonmul  19464  prmirred  19843  znfld  19909  lindfmm  20166  lindsmm  20167  lsslindf  20169  lsslinds  20170  islindf4  20177  basdif0  20757  neiptopreu  20937  neitr  20984  restlp  20987  cnrest2  21090  cnprest  21093  cnprest2  21094  lmss  21102  lmff  21105  ist1-2  21151  lpcls  21168  perfcls  21169  cmpfi  21211  hauseqlcld  21449  txlm  21451  txkgen  21455  xkopt  21458  idqtop  21509  tgqtop  21515  qtopcn  21517  uffix  21725  fmco  21765  flimrest  21787  lmflf  21809  txflf  21810  fclsrest  21828  cnpfcf  21845  tsmsgsum  21942  tsmsres  21947  tsmsf1o  21948  fmucndlem  22095  ismet2  22138  imasf1oxmet  22180  blres  22236  xmetec  22239  imasf1obl  22293  imasf1oxms  22294  prdsbl  22296  stdbdbl  22322  metrest  22329  metustsym  22360  blval2  22367  metuel2  22370  tngngp  22458  cnbl0  22577  cnblcld  22578  bl2ioo  22595  cncfcnvcn  22724  iihalf2  22732  icoopnst  22738  iocopnst  22739  icopnfcnv  22741  icopnfhmeo  22742  cphorthcom  23001  caucfil  23081  lmclim  23101  cmsss  23147  rrxmet  23191  volsup  23324  dyaddisjlem  23363  mbfeqalem  23409  mbfeqa  23410  mbfmulc2lem  23414  mbfmax  23416  mbfposr  23419  ismbf3d  23421  mbfimaopnlem  23422  mbfaddlem  23427  mbfsup  23431  mbfinf  23432  0plef  23439  0pledm  23440  i1fmulclem  23469  i1fres  23472  i1fpos  23473  itg1climres  23481  mbfi1fseqlem4  23485  itg2mulclem  23513  itg2monolem1  23517  itg2cnlem1  23528  iblre  23560  iblcn  23565  itgeqa  23580  ellimc2  23641  limcflf  23645  dvreslem  23673  lhop1  23777  ply1remlem  23922  fta1glem2  23926  ofmulrt  24037  plydiveu  24053  plyremlem  24059  quotcan  24064  ulmres  24142  cos11  24279  logleb  24349  argrege0  24357  logdivle  24368  efopn  24404  logccv  24409  cxplt  24440  cxple  24441  cxple2  24443  cxplt2  24444  cxplt3  24446  cxple3  24447  logbleb  24521  logblt  24522  angrtmuld  24538  quad2  24566  atans2  24658  rlimcnp  24692  rlimcnp2  24693  rlimcxp  24700  sqff1o  24908  fsumvma2  24939  dchrptlem2  24990  lgsdilem  25049  lgsne0  25060  lgsqr  25076  lgsquadlem1  25105  lgsquadlem2  25106  m1lgs  25113  2lgslem1a  25116  2lgs  25132  dchrisum0lem1  25205  padicabv  25319  trgcgrg  25410  colcom  25453  colrot1  25454  ishlg  25497  hlcomb  25498  hlbtwn  25506  lncom  25517  lnrot2  25519  israg  25592  perpcom  25608  hpgcom  25659  colopp  25661  iscgra  25701  isinag  25729  colinearalglem2  25787  axcgrid  25796  nbgrsym  26265  uvtxa01vtx0  26297  iscplgredg  26313  rgrusgrprc  26485  uspgr2wlkeq  26542  clwlkclwwlk  26903  eupth2lem3lem6  27093  fusgr2wsp2nb  27198  nmorepnf  27623  blocnilem  27659  ubthlem1  27726  shscom  28178  pjpreeq  28257  spansncol  28427  cmcm2  28475  hodsi  28634  nmoprepnf  28726  nmfnrepnf  28739  pjssposi  29031  cvcon3  29143  mdsymlem8  29269  dmdsym  29272  disjunsn  29407  fimarab  29445  unipreima  29446  fmptcof2  29457  1stpreima  29484  fpwrelmapffslem  29507  infxrge0gelb  29531  nndiffz1  29548  isinftm  29735  metidv  29935  metider  29937  pstmxmet  29940  xrge0iifiso  29981  indpi1  30082  prodindf  30085  indf1ofs  30088  aean  30307  brfae  30311  signsply0  30628  signsvfn  30659  reprinrn  30696  subfacp1lem3  31164  subfacp1lem5  31166  opelco3  31678  sscoid  32020  cgrcomr  32104  ofscom  32114  cgr3permute3  32154  cgr3permute1  32155  cgr3com  32160  colinearperm1  32169  colinearperm3  32170  outsideofcom  32235  opnbnd  32320  filnetlem4  32376  finxpsuclem  33234  wl-equsald  33325  wl-sbcom3  33372  poimirlem23  33432  broucube  33443  heicant  33444  itg2addnclem2  33462  ftc1anclem1  33485  ftc1anclem5  33489  ftc1anclem6  33490  areacirclem5  33504  areacirc  33505  caures  33556  cnpwstotbnd  33596  ismtyima  33602  rrnmet  33628  reheibor  33638  rngosn3  33723  lcvbr  34308  lkrsc  34384  lshpkrlem1  34397  opltcon3b  34491  cmt2N  34537  cmt3N  34538  cvrcon3b  34564  cvrcmp2  34571  cvlexchb2  34618  cvlatexchb2  34622  2llnmj  34846  4atlem3  34882  4atlem9  34889  4atlem10a  34890  4atlem11a  34893  4atlem12a  34896  4at2  34900  2lplnmj  34908  llnexchb2  35155  lautlt  35377  lautcvr  35378  lautco  35383  ltrnatb  35423  ltrneq2  35434  cdlemefrs29pre00  35683  cdlemefrs29cpre1  35686  cdleme32fva  35725  dibglbN  36455  dochsncom  36671  dochkrsat  36744  lspindp5  37059  mapdh8ab  37066  hdmapip0com  37209  lzenom  37333  rmxycomplete  37482  fzneg  37549  modabsdifz  37553  jm2.19  37560  pw2f1ocnv  37604  brtrclfv2  38019  rfovcnvf1od  38298  ntrclsfveq1  38358  ntrclsiso  38365  k0004lem2  38446  caofcan  38522  rfcnpre1  39178  rfcnpre2  39190  ellimcabssub0  39849  fperdvper  40133  vonvolmbl  40875  mgmpropd  41775  lco0  42216  lindslininds  42253  ltsubaddb  42304  ltsubsubb  42305  ltsubadd2b  42306  elbigolo1  42351  dig2bits  42408