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:  r19.12snOLD  4081  sbcbr  4490  fvopab3g  5937  fvimacnvALT  5991  respreima  6001  fmptco  6049  fnnfpeq0  6087  fnsuppresOLD  6116  cocan1  6179  cocan2  6180  ordsucelsuc  6642  ordsucsssuc  6643  fnsuppres  6929  smoword  7039  oaword  7200  omword  7221  om00el  7227  oeword  7241  nnaword  7278  nnmword  7284  swoer  7341  erth  7358  brecop  7406  eceqoveq  7418  xpdom2  7614  pw2f1olem  7623  omsucdomOLD  7715  fisucdomOLD  7725  ixpfi2  7820  wemapso2lem  7981  cantnfrescl  8098  rankr1bg  8224  r1pwcl  8268  fseqenlem1  8408  alephord3  8462  alephdom2  8471  engch  9009  fpwwe2lem7  9017  fpwwe2lem9  9019  ltexpi  9283  ltapi  9284  ltmpi  9285  ltsonq  9350  ltmnq  9353  1idpr  9410  addcanpr  9427  axpre-ltadd  9547  axlttri  9659  subsub23  9830  leadd1  10027  ltsub1  10055  ltsub2  10056  leord1  10087  eqord1  10088  lemul1  10401  lediv1  10414  lt2mul2div  10428  lerec  10434  lediv2  10442  le2msq  10452  suprleub  10514  infmrgelb  10530  ofsubeq0  10540  ofsubge0  10542  avgle1  10785  avgle2  10786  cnref1o  11226  xleneg  11428  xltadd1  11459  xsubge0  11464  xposdif  11465  xltmul1  11495  supxrleub  11529  infmxrgelb  11537  iooneg  11651  iccneg  11652  iccsplit  11664  iccshftr  11665  iccshftl  11667  iccdil  11669  icccntr  11671  fzsplit2  11721  fzaddel  11729  fzrev  11753  elfzo  11813  fzon  11829  elfzom1b  11893  negmod0  11986  leexp2  12202  ltexp2r  12204  repswsymball  12733  repswsymballbi  12734  cjreb  12938  sqrtlt  13077  limsuplt  13284  o1lo1  13342  rlimresb  13370  lo1eq  13373  rlimeq  13374  o1eq  13375  isercoll  13472  efle  13835  tanaddlem  13883  nndivdvds  13974  moddvds  13975  oddm1even  14029  bitsp1  14063  sadcaddlem  14089  sadadd  14099  sadass  14103  bitsshft  14107  smuval2  14114  smumul  14125  dvdssq  14180  phiprmpw  14288  eulerthlem2  14294  odzdvds  14304  pc2dvds  14384  1arith  14427  imasleval  14920  mreacs  15037  catpropd  15086  oppcsect  15150  funcres2b  15245  fthsect  15273  fthinv  15274  fucsect  15320  fucinv  15321  latnlemlt  15693  latnle  15694  ipole  15767  ipolt  15768  issubg3  16198  eqgid  16232  resghm2b  16264  conjghm  16276  gastacos  16327  resscntz  16348  cntzrec  16350  oppgsubm  16376  oppgsubg  16377  sylow3lem6  16631  lsmcom2  16654  lsmass  16667  lsmcomx  16841  subgdmdprd  17060  opprsubrg  17429  lsslss  17586  lbspropd  17724  islbs2  17779  rspsn  17881  psrbagconf1o  18005  gsumbagdiaglem  18006  mplmonmul  18105  prmirred  18503  prmirredOLD  18506  znfld  18577  lindfmm  18840  lindsmm  18841  lsslindf  18843  lsslinds  18844  islindf4  18851  basdif0  19432  neiptopreu  19612  neitr  19659  restlp  19662  cnrest2  19765  cnprest  19768  cnprest2  19769  lmss  19777  lmff  19780  ist1-2  19826  lpcls  19843  perfcls  19844  cmpfi  19886  hauseqlcld  20125  txlm  20127  txkgen  20131  xkopt  20134  idqtop  20185  tgqtop  20191  qtopcn  20193  uffix  20400  fmco  20440  flimrest  20462  lmflf  20484  txflf  20485  fclsrest  20503  cnpfcf  20520  tsmsgsum  20615  tsmsgsumOLD  20618  tsmsresOLD  20623  tsmsres  20624  tsmsf1o  20625  fmucndlem  20772  ismet2  20814  imasf1oxmet  20856  blres  20912  xmetec  20915  imasf1obl  20969  imasf1oxms  20970  prdsbl  20972  stdbdbl  20998  metrest  21005  metustsymOLD  21042  metustsym  21043  blval2  21056  metuel2  21060  tngngp  21146  cnbl0  21259  cnblcld  21260  bl2ioo  21275  cncfcnvcn  21403  iihalf2  21411  icoopnst  21417  iocopnst  21418  icopnfcnv  21420  icopnfhmeo  21421  cphorthcom  21625  caucfil  21700  lmclim  21719  cmsss  21767  rrxmet  21813  volsup  21944  dyaddisjlem  21982  mbfeqalem  22027  mbfeqa  22028  mbfmulc2lem  22032  mbfmax  22034  mbfposr  22037  ismbf3d  22039  mbfimaopnlem  22040  mbfaddlem  22045  mbfsup  22049  mbfinf  22050  0plef  22057  0pledm  22058  i1fmulclem  22087  i1fres  22090  i1fpos  22091  itg1climres  22099  mbfi1fseqlem4  22103  itg2mulclem  22131  itg2monolem1  22135  itg2cnlem1  22146  iblre  22178  iblcn  22183  itgeqa  22198  ellimc2  22259  limcflf  22263  dvreslem  22291  lhop1  22393  ply1remlem  22541  fta1glem2  22545  ofmulrt  22656  plydiveu  22672  plyremlem  22678  quotcan  22683  ulmres  22761  cos11  22898  logleb  22966  argrege0  22974  logdivle  22985  efopn  23017  logccv  23022  cxplt  23053  cxple  23054  cxple2  23056  cxplt2  23057  cxplt3  23059  cxple3  23060  angrtmuld  23118  quad2  23148  atans2  23240  rlimcnp  23273  rlimcnp2  23274  rlimcxp  23281  sqff1o  23434  fsumvma2  23467  dchrptlem2  23518  lgsdilem  23575  lgsne0  23586  lgsqr  23599  lgsquadlem1  23607  lgsquadlem2  23608  m1lgs  23615  dchrisum0lem1  23679  padicabv  23793  trgcgrg  23884  colcom  23923  colrot1  23924  ishlg  23964  hlcomb  23965  hlbtwn  23973  lncom  23980  lnrot2  23982  israg  24052  perpcom  24068  hpgcom  24114  iscgra  24147  colinearalglem2  24188  axcgrid  24197  uhgraeq12d  24285  usgraeq12d  24340  nbgrasym  24417  cusgrauvtxb  24474  usg2wlkeq  24686  clwlkisclwwlk  24767  eupath2lem3  24957  usg2spot2nb  25043  rngosn3  25406  nvsubsub23  25535  nmorepnf  25661  blocnilem  25697  ubthlem1  25764  shscom  26215  pjpreeq  26294  spansncol  26464  cmcm2  26512  hodsi  26672  nmoprepnf  26764  nmfnrepnf  26777  pjssposi  27069  cvcon3  27181  mdsymlem8  27307  dmdsym  27310  disjunsn  27431  fimarab  27461  unipreima  27462  fmptcof2  27480  1stpreima  27502  fpwrelmapffslem  27533  nndiffz1  27574  isinftm  27703  metidv  27849  metider  27851  pstmxmet  27854  xrge0iifiso  27895  logblt  28000  indpi1  28013  indf1ofs  28017  aean  28194  brfae  28198  signsply0  28486  signsvfn  28517  subfacp1lem3  28604  subfacp1lem5  28606  opelco3  29184  predfz  29259  sscoid  29539  cgrcomr  29623  ofscom  29633  cgr3permute3  29673  cgr3permute1  29674  cgr3com  29679  colinearperm1  29688  colinearperm3  29689  outsideofcom  29754  wl-equsald  29968  wl-sbcom3  30011  heicant  30025  itg2addnclem2  30043  ftc1anclem1  30066  ftc1anclem5  30070  ftc1anclem6  30071  areacirclem5  30087  areacirc  30088  opnbnd  30119  filnetlem4  30175  caures  30229  cnpwstotbnd  30269  ismtyima  30275  rrnmet  30301  reheibor  30311  lzenom  30679  rmxycomplete  30829  fzneg  30896  modabsdifz  30903  jm2.19  30911  pw2f1ocnv  30955  caofcan  31204  rfcnpre1  31348  rfcnpre2  31360  ellimcabssub0  31577  fperdvper  31669  pr1eqbg  32251  isfusgracl  32380  isfusgraclALT  32382  fusgraimpclALT2  32385  mgmpropd  32417  lco0  32898  lindslininds  32935  lcvbr  34621  lkrsc  34697  lshpkrlem1  34710  opltcon3b  34804  cmt2N  34850  cmt3N  34851  cvrcon3b  34877  cvrcmp2  34884  cvlexchb2  34931  cvlatexchb2  34935  2llnmj  35159  4atlem3  35195  4atlem9  35202  4atlem10a  35203  4atlem11a  35206  4atlem12a  35209  4at2  35213  2lplnmj  35221  llnexchb2  35468  lautlt  35690  lautcvr  35691  lautco  35696  ltrnatb  35736  ltrneq2  35747  cdlemefrs29pre00  35996  cdlemefrs29cpre1  35999  cdleme32fva  36038  dibglbN  36768  dochsncom  36984  dochkrsat  37057  lspindp5  37372  mapdh8ab  37379  hdmapip0com  37522