Theorem 3bitrd 279

Description: Deduction from transitivity of biconditional. (Contributed by NM, 13-Aug-1999.)

Hypotheses

Ref	Expression
3bitrd.1	|- ( ph -> ( ps <-> ch ) )
3bitrd.2	|- ( ph -> ( ch <-> th ) )
3bitrd.3	|- ( ph -> ( th <-> ta ) )

Assertion

Ref	Expression
3bitrd	|- ( ph -> ( ps <-> ta ) )

Proof of Theorem 3bitrd

Step	Hyp	Ref	Expression
1		3bitrd.1	. . 3 |- ( ph -> ( ps <-> ch ) )
2		3bitrd.2	. . 3 |- ( ph -> ( ch <-> th ) )
3	1, 2	bitrd 253	. 2 |- ( ph -> ( ps <-> th ) )
4		3bitrd.3	. 2 |- ( ph -> ( th <-> ta ) )
5	3, 4	bitrd 253	1 |- ( ph -> ( ps <-> 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:  sbceqal  3387  elimhyp3v  4000  elimhyp4v  4001  keephyp3v  4006  opelopabgf  4767  f1eq123d  5809  foeq123d  5810  f1oeq123d  5811  fnmptfvd  5982  ofrfval  6530  eloprabi  6843  fnmpt2ovd  6858  suppsnop  6912  smoeq  7018  wemapwe  8135  wemapweOLD  8136  fseqenlem1  8401  dfac12lem2  8520  fin23lem22  8703  pwfseqlem5  9037  pwfseq  9038  enqbreq2  9294  lterpq  9344  ltdiv23  10432  lediv23  10433  halfpos  10765  addltmul  10770  supminf  11165  supxrbnd1  11509  supxrbnd2  11510  iccf1o  11660  fzshftral  11761  fzoshftral  11887  dfceil2  11932  modirr  12021  hashen1  12403  seqcoll  12474  s111  12582  swrdeq  12630  wrdeqswrdlsw  12633  wrd2ind  12662  2swrd2eqwrdeq  12850  limsupgle  13259  tanaddlem  13758  dvdssub  13881  dvdsmod  13898  oddp1even  13903  bitscmp  13943  saddisjlem  13969  smueqlem  13995  prmreclem5  14293  4sqlem11  14328  4sqlem17  14334  vdwmc2  14352  ismre  14841  acsfn  14910  isssc  15046  setcinv  15271  nmzsubg  16037  conjnmzb  16096  gsmsymgreqlem2  16251  symgfixels  16254  f1omvdconj  16267  oddvdsnn0  16364  oddvds  16367  odcong  16369  odf1  16380  dpjeq  16898  dpjeqOLD  16905  pgpfac1lem2  16916  lsmspsn  17513  lbsacsbs  17585  lpigen  17686  prmirredlem  18290  prmirredlemOLD  18293  znf1o  18357  znleval  18360  znunit  18369  islinds2  18615  islindf4  18640  scmatf1  18800  isclo  19354  maxlp  19414  1stccn  19730  xkoinjcn  19923  elmptrab  20063  fbunfip  20105  elfm  20183  fmid  20196  flfnei  20227  isflf  20229  isfcls  20245  fclsopn  20250  isfcf  20270  cnextfun  20299  eltsms  20366  prdsxmetlem  20606  elmopn  20680  metss  20746  comet  20751  elbl4  20814  metuel2  20817  nrmmetd  20830  metdsge  21088  tchcph  21415  fmcfil  21446  minveclem4  21582  shft2rab  21654  sca2rab  21658  volsup2  21749  mbfsup  21806  i1fmullem  21836  mbfi1fseqlem4  21860  xrge0f  21873  itg2monolem1  21892  ellimc2  22016  cnlimc  22027  mdegleb  22199  facth1  22300  ulm2  22514  sineq0  22647  coseq1  22648  efeq1  22649  sinord  22654  root1eq1  22857  angrtmuld  22868  quad2  22898  dcubic  22905  cubic2  22907  dquartlem1  22910  dquart  22912  quart  22920  rlimcnp  23023  mumullem2  23182  chtub  23215  fsumvma  23216  fsumvma2  23217  chpchtsum  23222  bposlem7  23293  lgsneg  23322  lgsne0  23336  lgsqrlem2  23345  lgsquadlem1  23357  lgsquadlem2  23358  axcontlem7  23949  isuslgra  24019  isusgra  24020  ausisusgra  24031  nbgraopALT  24100  nb3graprlem2  24128  cusgra3v  24140  sizeusglecusg  24162  uvtx01vtx  24168  is2wlk  24243  0pth  24248  wlkdvspthlem  24285  2wlkeq  24383  wwlknextbi  24401  clwwlkn2  24451  el2wlkonotot0  24548  el2wlkonotot  24549  el2wlksoton  24554  el2spthsoton  24555  el2wlksot  24556  el2pthsot  24557  isrusgusrgcl  24609  rusgrasn  24621  rusgranumwlkl1  24623  rusgra0edg  24631  eupath2lem2  24654  eupath2lem3  24655  frgra2v  24675  frgra3v  24678  usg2spot2nb  24742  numclwwlkovfel2  24760  numclwwlk2lem1  24779  numclwlk2lem2f1o  24782  frgrareggt1  24793  isass  24994  rngosn3  25104  imsmetlem  25272  ipz  25308  bnsscmcl  25460  minvecolem4  25472  hvsubcan  25667  hoeq2  26426  leoptri  26731  atcv0eq  26974  elimifd  27095  gtiso  27191  2ndpreima  27197  fpwrelmapffslem  27227  fzsplit3  27267  isomnd  27353  ogrpinvlt  27376  pstmfval  27511  lmlim  27565  dya2ub  27881  eulerpartlemr  27953  isrrvv  28022  ballotlemsima  28094  signsvfn  28179  lgamucov  28220  subfacp1lem3  28266  subfacp1lem5  28268  erdszelem1  28275  erdsze  28286  erdsze2lem2  28288  elpredg  28835  dvtanlem  29641  itg2addnclem2  29644  ftc1anclem1  29667  areacirclem1  29684  areacirclem5  29688  filnetlem4  29802  metf1o  29851  elrfirn  30231  jm2.19lem2  30536  proot1ex  30766  ellimcabssub0  31159  fperdvper  31248  fourierdlem113  31520  2reu4a  31661  ltnltne  31790  islindeps  32127  snlindsntor  32145  mnd1  32161  bj-issetwt  33516  bj-sbceqgALT  33550  lsatcv0eq  33844  cmtbr2N  34050  atlatmstc  34116  1cvrco  34268  cdleme3  35033  cdleme7  35045  cdlemg10c  35435  dvhopellsm  35914  dibord  35956  dib1dim2  35965  diblsmopel  35968  dihopelvalcpre  36045  dih1dimatlem  36126  hdmap14lem13  36680  hdmapoc  36731