Theorem 3bitr4d 293

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

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

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 190

This theorem is referenced by:  sbcbr  4448  fvopab3g  5959  fvimacnvALT  6016  respreima  6024  fmptco  6072  fnnfpeq0  6111  cocan1  6207  cocan2  6208  ordsucelsuc  6668  ordsucsssuc  6669  fnsuppres  6961  smoword  7103  oaword  7268  omword  7289  om00el  7295  oeword  7309  nnaword  7346  nnmword  7352  swoer  7409  erth  7426  brecop  7474  eceqoveq  7486  xpdom2  7685  pw2f1olem  7694  ixpfi2  7890  wemapso2lem  8085  cantnfrescl  8199  rankr1bg  8292  r1pwcl  8336  fseqenlem1  8473  alephord3  8527  alephdom2  8536  engch  9071  fpwwe2lem7  9079  fpwwe2lem9  9081  ltexpi  9345  ltapi  9346  ltmpi  9347  ltsonq  9412  ltmnq  9415  1idpr  9472  addcanpr  9489  axpre-ltadd  9609  axlttri  9723  subsub23  9900  leadd1  10103  ltsub1  10131  ltsub2  10132  leord1  10162  eqord1  10163  lemul1  10479  lediv1  10492  lt2mul2div  10505  lerec  10511  lediv2  10518  le2msq  10528  suprleub  10595  infregelb  10616  infmrgelbOLD  10617  ofsubeq0  10628  ofsubge0  10630  avgle1  10875  avgle2  10876  cnref1o  11320  xleneg  11534  xltadd1  11567  xsubge0  11572  xposdif  11573  xltmul1  11603  supxrleub  11637  infxrgelb  11646  infmxrgelbOLD  11650  iooneg  11778  iccneg  11779  iccsplit  11791  iccshftr  11792  iccshftl  11794  iccdil  11796  icccntr  11798  fzsplit2  11850  fzaddel  11859  fzrev  11884  predfz  11941  elfzo  11949  nelfzo  11952  fzon  11966  elfzom1b  12039  negmod0  12138  leexp2  12365  ltexp2r  12367  repswsymball  12936  repswsymballbi  12937  cjreb  13263  sqrtlt  13402  limsuplt  13615  limsupltOLD  13616  o1lo1  13678  rlimresb  13706  lo1eq  13709  rlimeq  13710  o1eq  13711  isercoll  13808  efle  14249  tanaddlem  14297  nndivdvds  14388  moddvds  14389  oddm1even  14444  bitsp1  14483  sadcaddlem  14510  sadadd  14520  sadass  14524  bitsshft  14528  smuval2  14535  smumul  14546  dvdssq  14607  phiprmpw  14803  eulerthlem2  14809  odzdvds  14819  odzdvdsOLD  14825  pc2dvds  14907  1arith  14950  imasleval  15525  mreacs  15642  catpropd  15692  oppcsect  15761  funcres2b  15880  fthsect  15908  fthinv  15909  fucsect  15955  fucinv  15956  latnlemlt  16408  latnle  16409  ipole  16482  ipolt  16483  issubg3  16913  eqgid  16947  resghm2b  16979  conjghm  16991  gastacos  17042  resscntz  17063  cntzrec  17065  oppgsubm  17091  oppgsubg  17092  sylow3lem6  17362  lsmcom2  17385  lsmass  17398  lsmcomx  17572  subgdmdprd  17745  opprsubrg  18107  lsslss  18262  lbspropd  18400  islbs2  18455  rspsn  18555  psrbagconf1o  18675  gsumbagdiaglem  18676  mplmonmul  18765  prmirred  19143  znfld  19208  lindfmm  19462  lindsmm  19463  lsslindf  19465  lsslinds  19466  islindf4  19473  basdif0  20045  neiptopreu  20226  neitr  20273  restlp  20276  cnrest2  20379  cnprest  20382  cnprest2  20383  lmss  20391  lmff  20394  ist1-2  20440  lpcls  20457  perfcls  20458  cmpfi  20500  hauseqlcld  20738  txlm  20740  txkgen  20744  xkopt  20747  idqtop  20798  tgqtop  20804  qtopcn  20806  uffix  21014  fmco  21054  flimrest  21076  lmflf  21098  txflf  21099  fclsrest  21117  cnpfcf  21134  tsmsgsum  21231  tsmsres  21236  tsmsf1o  21237  fmucndlem  21384  ismet2  21426  imasf1oxmet  21468  blres  21524  xmetec  21527  imasf1obl  21581  imasf1oxms  21582  prdsbl  21584  stdbdbl  21610  metrest  21617  metustsym  21648  blval2  21655  metuel2  21658  tngngp  21740  cnbl0  21872  cnblcld  21873  bl2ioo  21888  cncfcnvcn  22031  iihalf2  22039  icoopnst  22045  iocopnst  22046  icopnfcnv  22048  icopnfhmeo  22049  cphorthcom  22256  caucfil  22331  lmclim  22350  cmsss  22396  rrxmet  22440  volsup  22588  dyaddisjlem  22632  mbfeqalem  22677  mbfeqa  22678  mbfmulc2lem  22682  mbfmax  22684  mbfposr  22687  ismbf3d  22689  mbfimaopnlem  22690  mbfaddlem  22695  mbfsup  22699  mbfinf  22700  mbfinfOLD  22701  0plef  22709  0pledm  22710  i1fmulclem  22739  i1fres  22742  i1fpos  22743  itg1climres  22751  mbfi1fseqlem4  22755  itg2mulclem  22783  itg2monolem1  22787  itg2cnlem1  22798  iblre  22830  iblcn  22835  itgeqa  22850  ellimc2  22911  limcflf  22915  dvreslem  22943  lhop1  23045  ply1remlem  23192  fta1glem2  23196  ofmulrt  23314  plydiveu  23330  plyremlem  23336  quotcan  23341  ulmres  23422  cos11  23561  logleb  23631  argrege0  23639  logdivle  23650  efopn  23682  logccv  23687  cxplt  23718  cxple  23719  cxple2  23721  cxplt2  23722  cxplt3  23724  cxple3  23725  logbleb  23799  logblt  23800  angrtmuld  23816  quad2  23844  atans2  23936  rlimcnp  23970  rlimcnp2  23971  rlimcxp  23978  sqff1o  24188  fsumvma2  24221  dchrptlem2  24272  lgsdilem  24329  lgsne0  24340  lgsqr  24353  lgsquadlem1  24361  lgsquadlem2  24362  m1lgs  24369  dchrisum0lem1  24433  padicabv  24547  trgcgrg  24639  colcom  24682  colrot1  24683  ishlg  24726  hlcomb  24727  hlbtwn  24735  lncom  24746  lnrot2  24748  israg  24821  perpcom  24837  hpgcom  24888  colopp  24890  iscgra  24930  isinag  24958  colinearalglem2  25016  axcgrid  25025  uhgraeq12d  25113  usgraeq12d  25168  nbgrasym  25246  cusgrauvtxb  25303  usg2wlkeq  25515  clwlkisclwwlk  25596  eupath2lem3  25786  usg2spot2nb  25872  rngosn3  26235  nvsubsub23  26364  nmorepnf  26490  blocnilem  26526  ubthlem1  26593  shscom  27053  pjpreeq  27132  spansncol  27302  cmcm2  27350  hodsi  27509  nmoprepnf  27601  nmfnrepnf  27614  pjssposi  27906  cvcon3  28018  mdsymlem8  28144  dmdsym  28147  disjunsn  28281  fimarab  28320  unipreima  28321  fmptcof2  28334  1stpreima  28362  fpwrelmapffslem  28392  infxrge0gelb  28425  infxrge0gelbOLD  28426  nndiffz1  28441  isinftm  28572  metidv  28769  metider  28771  pstmxmet  28774  xrge0iifiso  28815  indpi1  28917  indf1ofs  28921  aean  29140  brfae  29144  signsply0  29512  signsvfn  29543  subfacp1lem3  29977  subfacp1lem5  29979  opelco3  30491  sscoid  30751  cgrcomr  30835  ofscom  30845  cgr3permute3  30885  cgr3permute1  30886  cgr3com  30891  colinearperm1  30900  colinearperm3  30901  outsideofcom  30966  opnbnd  31052  filnetlem4  31108  finxpsuclem  31859  wl-equsald  31942  wl-sbcom3  31989  poimirlem23  32027  broucube  32038  heicant  32039  itg2addnclem2  32058  ftc1anclem1  32081  ftc1anclem5  32085  ftc1anclem6  32086  areacirclem5  32100  areacirc  32101  caures  32153  cnpwstotbnd  32193  ismtyima  32199  rrnmet  32225  reheibor  32235  lcvbr  32658  lkrsc  32734  lshpkrlem1  32747  opltcon3b  32841  cmt2N  32887  cmt3N  32888  cvrcon3b  32914  cvrcmp2  32921  cvlexchb2  32968  cvlatexchb2  32972  2llnmj  33196  4atlem3  33232  4atlem9  33239  4atlem10a  33240  4atlem11a  33243  4atlem12a  33246  4at2  33250  2lplnmj  33258  llnexchb2  33505  lautlt  33727  lautcvr  33728  lautco  33733  ltrnatb  33773  ltrneq2  33784  cdlemefrs29pre00  34033  cdlemefrs29cpre1  34036  cdleme32fva  34075  dibglbN  34805  dochsncom  35021  dochkrsat  35094  lspindp5  35409  mapdh8ab  35416  hdmapip0com  35559  lzenom  35683  rmxycomplete  35836  fzneg  35903  modabsdifz  35910  jm2.19  35919  pw2f1ocnv  35963  brtrclfv2  36390  caofcan  36742  rfcnpre1  37403  rfcnpre2  37415  ellimcabssub0  37794  fperdvper  37887  vonvolmbl  38601  pr1eqbg  39138  nbgrsym  39601  uvtxa01vtx0  39633  iscplgredg  39649  rgrusgrprc  39793  eupth2lem3lem6  40145  isfusgracl  40246  isfusgraclALT  40248  fusgraimpclALT2  40251  mgmpropd  40283  lco0  40728  lindslininds  40765  ltsubaddb  40819  ltsubsubb  40820  ltsubadd2b  40821  elbigolo1  40876  dig2bits  40933