Theorem 3bitr4d 277

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

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

This theorem is referenced by:  sbcom  2138  sbcom2  2163  r19.12sn  3832  ordsucelsuc  4761  ordsucsssuc  4762  fvopab3g  5761  fvimacnvALT  5808  respreima  5818  fmptco  5860  fnsuppres  5911  cocan1  5983  cocan2  5984  smoword  6587  oaword  6751  omword  6772  om00el  6778  oeword  6792  nnaword  6829  nnmword  6835  swoer  6892  erth  6908  brecop  6956  eceqoveq  6968  xpdom2  7162  pw2f1olem  7171  omsucdomOLD  7261  fisucdomOLD  7271  ixpfi2  7363  cantnfrescl  7588  rankr1bg  7685  r1pwcl  7729  fseqenlem1  7861  alephord3  7915  alephdom2  7924  engch  8459  fpwwe2lem7  8467  fpwwe2lem9  8469  ltexpi  8735  ltapi  8736  ltmpi  8737  ltsonq  8802  ltmnq  8805  1idpr  8862  addcanpr  8879  axpre-ltadd  8998  axlttri  9103  subsub23  9266  leadd1  9452  ltsub1  9480  ltsub2  9481  leord1  9510  eqord1  9511  lemul1  9818  lediv1  9831  lt2mul2div  9842  lerec  9848  lediv2  9856  le2msq  9866  suprleub  9928  infmrgelb  9944  ofsubeq0  9953  ofsubge0  9955  avgle1  10163  avgle2  10164  cnref1o  10563  xleneg  10760  xltadd1  10791  xsubge0  10796  xposdif  10797  xltmul1  10827  supxrleub  10861  infmxrgelb  10869  iooneg  10973  iccneg  10974  iccsplit  10985  iccshftr  10986  iccshftl  10988  iccdil  10990  icccntr  10992  fzsplit2  11032  fzaddel  11043  fzrev  11064  elfzo  11097  fzon  11113  elfzom1b  11146  negmod0  11211  leexp2  11389  ltexp2r  11391  cjreb  11883  sqrlt  12022  rexfiuz  12106  limsuplt  12228  o1lo1  12286  rlimresb  12314  lo1eq  12317  rlimeq  12318  o1eq  12319  isercoll  12416  efle  12674  tanaddlem  12722  nndivdvds  12813  moddvds  12814  oddm1even  12864  bitsp1  12898  sadcaddlem  12924  sadadd  12934  sadass  12938  bitsshft  12942  smuval2  12949  smumul  12960  dvdssq  13015  phiprmpw  13120  eulerthlem2  13126  odzdvds  13136  pc2dvds  13207  1arith  13250  imasleval  13721  mreacs  13838  catpropd  13890  oppcsect  13954  funcres2b  14049  fthsect  14077  fthinv  14078  fucsect  14124  fucinv  14125  latnlemlt  14468  latnle  14469  ipole  14539  ipolt  14540  spwex  14616  issubg3  14915  eqgid  14947  resghm2b  14979  conjghm  14991  gastacos  15042  resscntz  15085  cntzrec  15087  oppgsubm  15113  oppgsubg  15114  sylow3lem6  15221  lsmcom2  15244  lsmass  15257  lsmcomx  15426  subgdmdprd  15547  opprsubrg  15844  lsslss  15992  lbspropd  16126  islbs2  16181  rspsn  16280  psrbagconf1o  16394  gsumbagdiaglem  16395  mplmonmul  16482  prmirred  16730  znfld  16796  basdif0  16973  neiptopreu  17152  neitr  17198  restlp  17201  cnrest2  17304  cnprest  17307  cnprest2  17308  lmss  17316  lmff  17319  ist1-2  17365  lpcls  17382  perfcls  17383  cmpfi  17425  hauseqlcld  17631  txlm  17633  txkgen  17637  xkopt  17640  idqtop  17691  tgqtop  17697  qtopcn  17699  uffix  17906  fmco  17946  flimrest  17968  lmflf  17990  txflf  17991  fclsrest  18009  cnpfcf  18026  tsmsgsum  18121  tsmsres  18126  tsmsf1o  18127  fmucndlem  18274  ismet2  18316  imasf1oxmet  18358  blres  18414  xmetec  18417  imasf1obl  18471  imasf1oxms  18472  prdsbl  18474  stdbdbl  18500  metrest  18507  metustsymOLD  18544  metustsym  18545  blval2  18558  metuel2  18562  tngngp  18648  cnbl0  18761  cnblcld  18762  bl2ioo  18776  cncfcnvcn  18904  iihalf2  18911  icoopnst  18917  iocopnst  18918  icopnfcnv  18920  icopnfhmeo  18921  cphorthcom  19116  caucfil  19189  lmclim  19208  cmsss  19256  volsup  19403  dyaddisjlem  19440  mbfeqalem  19487  mbfeqa  19488  mbfmulc2lem  19492  mbfmax  19494  mbfposr  19497  ismbf3d  19499  mbfimaopnlem  19500  mbfaddlem  19505  mbfsup  19509  mbfinf  19510  0plef  19517  0pledm  19518  i1fmulclem  19547  i1fres  19550  i1fpos  19551  itg1climres  19559  mbfi1fseqlem4  19563  itg2mulclem  19591  itg2monolem1  19595  itg2cnlem1  19606  iblre  19638  iblcn  19643  itgeqa  19658  ellimc2  19717  limcflf  19721  dvreslem  19749  lhop1  19851  ply1remlem  20038  fta1glem2  20042  ofmulrt  20152  plydiveu  20168  plyremlem  20174  quotcan  20179  ulmres  20257  cos11  20388  logleb  20451  argrege0  20459  logdivle  20470  efopn  20502  logccv  20507  cxplt  20538  cxple  20539  cxple2  20541  cxplt2  20542  cxplt3  20544  cxple3  20545  angrtmuld  20603  quad2  20632  atans2  20724  rlimcnp  20757  rlimcnp2  20758  rlimcxp  20765  sqff1o  20918  fsumvma2  20951  dchrptlem2  21002  lgsdilem  21059  lgsne0  21070  lgsqr  21083  lgsquadlem1  21091  lgsquadlem2  21092  m1lgs  21099  dchrisum0lem1  21163  padicabv  21277  uhgraeq12d  21295  usgraeq12d  21338  nbgrasym  21402  cusgrauvtxb  21458  eupath2lem3  21654  rngosn3  21967  nvsubsub23  22096  nmorepnf  22222  blocnilem  22258  ubthlem1  22325  shscom  22774  pjpreeq  22853  spansncol  23023  cmcm2  23071  hodsi  23231  nmoprepnf  23323  nmfnrepnf  23336  pjssposi  23628  cvcon3  23740  mdsymlem8  23866  dmdsym  23869  unipreima  24009  fmptcof2  24029  1stpreima  24048  metider  24242  pstmxmet  24245  xrge0iifiso  24274  logblt  24359  indpi1  24372  indf1ofs  24376  aean  24548  brfae  24552  subfacp1lem3  24821  subfacp1lem5  24823  predfz  25417  elfuns  25668  colinearalglem2  25750  axcgrid  25759  cgrcomr  25835  ofscom  25845  cgr3permute3  25885  cgr3permute1  25886  cgr3com  25891  colinearperm1  25900  colinearperm3  25901  outsideofcom  25966  itg2addnclem2  26156  areacirclem6  26186  areacirc  26187  opnbnd  26218  filnetlem4  26300  caures  26356  cnpwstotbnd  26396  ismtyima  26402  rrnmet  26428  reheibor  26438  fnnfpeq0  26629  lzenom  26718  rmxycomplete  26870  fzneg  26937  modabsdifz  26946  jm2.19  26954  pw2f1ocnv  26998  lindfmm  27165  lindsmm  27166  lsslindf  27168  lsslinds  27169  islindf4  27176  caofcan  27408  rfcnpre1  27557  rfcnpre2  27569  pr1eqbg  27944  usg2spot2nb  28168  sbcomwAUX7  29291  sbcomOLD7  29439  sbcom2OLD7  29445  lcvbr  29504  lkrsc  29580  lshpkrlem1  29593  opltcon3b  29687  cmt2N  29733  cmt3N  29734  cvrcon3b  29760  cvrcmp2  29767  cvlexchb2  29814  cvlatexchb2  29818  2llnmj  30042  4atlem3  30078  4atlem9  30085  4atlem10a  30086  4atlem11a  30089  4atlem12a  30092  4at2  30096  2lplnmj  30104  llnexchb2  30351  lautlt  30573  lautcvr  30574  lautco  30579  ltrnatb  30619  ltrneq2  30630  cdlemefrs29pre00  30877  cdlemefrs29cpre1  30880  cdleme32fva  30919  dibglbN  31649  dochsncom  31865  dochkrsat  31938  lspindp5  32253  mapdh8ab  32260  hdmapip0com  32403

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8

This theorem depends on definitions:  df-bi 178