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:  sbcom2OLD  2161  r19.12sn  4048  sbcbr  4452  fvopab3g  5878  fvimacnvALT  5930  respreima  5940  fmptco  5984  fnnfpeq0  6017  fnsuppresOLD  6046  cocan1  6103  cocan2  6104  ordsucelsuc  6542  ordsucsssuc  6543  fnsuppres  6825  smoword  6936  oaword  7097  omword  7118  om00el  7124  oeword  7138  nnaword  7175  nnmword  7181  swoer  7238  erth  7254  brecop  7302  eceqoveq  7314  xpdom2  7515  pw2f1olem  7524  omsucdomOLD  7616  fisucdomOLD  7626  ixpfi2  7719  wemapso2lem  7877  cantnfrescl  7994  rankr1bg  8120  r1pwcl  8164  fseqenlem1  8304  alephord3  8358  alephdom2  8367  engch  8905  fpwwe2lem7  8913  fpwwe2lem9  8915  ltexpi  9181  ltapi  9182  ltmpi  9183  ltsonq  9248  ltmnq  9251  1idpr  9308  addcanpr  9325  axpre-ltadd  9444  axlttri  9556  subsub23  9725  leadd1  9917  ltsub1  9945  ltsub2  9946  leord1  9977  eqord1  9978  lemul1  10291  lediv1  10304  lt2mul2div  10318  lerec  10324  lediv2  10332  le2msq  10342  suprleub  10404  infmrgelb  10420  ofsubeq0  10429  ofsubge0  10431  avgle1  10674  avgle2  10675  cnref1o  11096  xleneg  11298  xltadd1  11329  xsubge0  11334  xposdif  11335  xltmul1  11365  supxrleub  11399  infmxrgelb  11407  iooneg  11521  iccneg  11522  iccsplit  11534  iccshftr  11535  iccshftl  11537  iccdil  11539  icccntr  11541  fzsplit2  11590  fzaddel  11609  fzrev  11635  elfzo  11671  fzon  11687  elfzom1b  11742  negmod0  11832  leexp2  12034  ltexp2r  12036  repswsymball  12534  repswsymballbi  12535  cjreb  12729  sqrlt  12868  limsuplt  13074  o1lo1  13132  rlimresb  13160  lo1eq  13163  rlimeq  13164  o1eq  13165  isercoll  13262  efle  13519  tanaddlem  13567  nndivdvds  13658  moddvds  13659  oddm1even  13710  bitsp1  13744  sadcaddlem  13770  sadadd  13780  sadass  13784  bitsshft  13788  smuval2  13795  smumul  13806  dvdssq  13861  phiprmpw  13968  eulerthlem2  13974  odzdvds  13984  pc2dvds  14062  1arith  14105  imasleval  14597  mreacs  14714  catpropd  14766  oppcsect  14830  funcres2b  14925  fthsect  14953  fthinv  14954  fucsect  15000  fucinv  15001  latnlemlt  15372  latnle  15373  ipole  15446  ipolt  15447  issubg3  15817  eqgid  15851  resghm2b  15883  conjghm  15895  gastacos  15946  resscntz  15967  cntzrec  15969  oppgsubm  15995  oppgsubg  15996  sylow3lem6  16251  lsmcom2  16274  lsmass  16287  lsmcomx  16458  subgdmdprd  16652  opprsubrg  17008  lsslss  17164  lbspropd  17302  islbs2  17357  rspsn  17458  psrbagconf1o  17566  gsumbagdiaglem  17567  mplmonmul  17666  prmirred  18043  prmirredOLD  18046  znfld  18117  lindfmm  18380  lindsmm  18381  lsslindf  18383  lsslinds  18384  islindf4  18391  basdif0  18689  neiptopreu  18868  neitr  18915  restlp  18918  cnrest2  19021  cnprest  19024  cnprest2  19025  lmss  19033  lmff  19036  ist1-2  19082  lpcls  19099  perfcls  19100  cmpfi  19142  hauseqlcld  19350  txlm  19352  txkgen  19356  xkopt  19359  idqtop  19410  tgqtop  19416  qtopcn  19418  uffix  19625  fmco  19665  flimrest  19687  lmflf  19709  txflf  19710  fclsrest  19728  cnpfcf  19745  tsmsgsum  19840  tsmsgsumOLD  19843  tsmsresOLD  19848  tsmsres  19849  tsmsf1o  19850  fmucndlem  19997  ismet2  20039  imasf1oxmet  20081  blres  20137  xmetec  20140  imasf1obl  20194  imasf1oxms  20195  prdsbl  20197  stdbdbl  20223  metrest  20230  metustsymOLD  20267  metustsym  20268  blval2  20281  metuel2  20285  tngngp  20371  cnbl0  20484  cnblcld  20485  bl2ioo  20500  cncfcnvcn  20628  iihalf2  20636  icoopnst  20642  iocopnst  20643  icopnfcnv  20645  icopnfhmeo  20646  cphorthcom  20850  caucfil  20925  lmclim  20944  cmsss  20992  rrxmet  21038  volsup  21169  dyaddisjlem  21207  mbfeqalem  21252  mbfeqa  21253  mbfmulc2lem  21257  mbfmax  21259  mbfposr  21262  ismbf3d  21264  mbfimaopnlem  21265  mbfaddlem  21270  mbfsup  21274  mbfinf  21275  0plef  21282  0pledm  21283  i1fmulclem  21312  i1fres  21315  i1fpos  21316  itg1climres  21324  mbfi1fseqlem4  21328  itg2mulclem  21356  itg2monolem1  21360  itg2cnlem1  21371  iblre  21403  iblcn  21408  itgeqa  21423  ellimc2  21484  limcflf  21488  dvreslem  21516  lhop1  21618  ply1remlem  21766  fta1glem2  21770  ofmulrt  21880  plydiveu  21896  plyremlem  21902  quotcan  21907  ulmres  21985  cos11  22121  logleb  22184  argrege0  22192  logdivle  22203  efopn  22235  logccv  22240  cxplt  22271  cxple  22272  cxple2  22274  cxplt2  22275  cxplt3  22277  cxple3  22278  angrtmuld  22336  quad2  22366  atans2  22458  rlimcnp  22491  rlimcnp2  22492  rlimcxp  22499  sqff1o  22652  fsumvma2  22685  dchrptlem2  22736  lgsdilem  22793  lgsne0  22804  lgsqr  22817  lgsquadlem1  22825  lgsquadlem2  22826  m1lgs  22833  dchrisum0lem1  22897  padicabv  23011  trgcgrg  23102  colcom  23127  colrot1  23128  lncom  23166  lnrot2  23168  israg  23233  perpcom  23248  colinearalglem2  23304  axcgrid  23313  uhgraeq12d  23392  usgraeq12d  23435  nbgrasym  23499  cusgrauvtxb  23555  eupath2lem3  23751  rngosn3  24064  nvsubsub23  24193  nmorepnf  24319  blocnilem  24355  ubthlem1  24422  shscom  24873  pjpreeq  24952  spansncol  25122  cmcm2  25170  hodsi  25330  nmoprepnf  25422  nmfnrepnf  25435  pjssposi  25727  cvcon3  25839  mdsymlem8  25965  dmdsym  25968  disjunsn  26086  unipreima  26111  fmptcof2  26129  1stpreima  26151  fpwrelmapffslem  26182  nndiffz1  26219  metider  26465  pstmxmet  26468  xrge0iifiso  26509  logblt  26609  indpi1  26622  indf1ofs  26626  aean  26803  brfae  26807  signsply0  27095  signsvfn  27126  subfacp1lem3  27213  subfacp1lem5  27215  opelco3  27732  predfz  27807  sscoid  28087  cgrcomr  28171  ofscom  28181  cgr3permute3  28221  cgr3permute1  28222  cgr3com  28227  colinearperm1  28236  colinearperm3  28237  outsideofcom  28302  wl-equsald  28515  wl-sbcom3  28558  heicant  28573  itg2addnclem2  28591  ftc1anclem1  28614  ftc1anclem5  28618  ftc1anclem6  28619  areacirclem5  28635  areacirc  28636  opnbnd  28667  filnetlem4  28749  caures  28803  cnpwstotbnd  28843  ismtyima  28849  rrnmet  28875  reheibor  28885  lzenom  29255  rmxycomplete  29405  fzneg  29472  modabsdifz  29481  jm2.19  29489  pw2f1ocnv  29533  caofcan  29744  rfcnpre1  29888  rfcnpre2  29900  pr1eqbg  30268  usg2wlkeq  30436  clwlkisclwwlk  30598  usg2spot2nb  30805  lco0  31079  lindslininds  31116  lcvbr  32989  lkrsc  33065  lshpkrlem1  33078  opltcon3b  33172  cmt2N  33218  cmt3N  33219  cvrcon3b  33245  cvrcmp2  33252  cvlexchb2  33299  cvlatexchb2  33303  2llnmj  33527  4atlem3  33563  4atlem9  33570  4atlem10a  33571  4atlem11a  33574  4atlem12a  33577  4at2  33581  2lplnmj  33589  llnexchb2  33836  lautlt  34058  lautcvr  34059  lautco  34064  ltrnatb  34104  ltrneq2  34115  cdlemefrs29pre00  34362  cdlemefrs29cpre1  34365  cdleme32fva  34404  dibglbN  35134  dochsncom  35350  dochkrsat  35423  lspindp5  35738  mapdh8ab  35745  hdmapip0com  35888