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  2152  r19.12sn  3936  sbcbr  4340  fvopab3g  5765  fvimacnvALT  5817  respreima  5827  fmptco  5871  fnnfpeq0  5904  fnsuppresOLD  5933  cocan1  5990  cocan2  5991  ordsucelsuc  6428  ordsucsssuc  6429  fnsuppres  6711  smoword  6819  oaword  6980  omword  7001  om00el  7007  oeword  7021  nnaword  7058  nnmword  7064  swoer  7121  erth  7137  brecop  7185  eceqoveq  7197  xpdom2  7398  pw2f1olem  7407  omsucdomOLD  7498  fisucdomOLD  7508  ixpfi2  7601  wemapso2lem  7759  cantnfrescl  7876  rankr1bg  8002  r1pwcl  8046  fseqenlem1  8186  alephord3  8240  alephdom2  8249  engch  8787  fpwwe2lem7  8795  fpwwe2lem9  8797  ltexpi  9063  ltapi  9064  ltmpi  9065  ltsonq  9130  ltmnq  9133  1idpr  9190  addcanpr  9207  axpre-ltadd  9326  axlttri  9438  subsub23  9607  leadd1  9799  ltsub1  9827  ltsub2  9828  leord1  9859  eqord1  9860  lemul1  10173  lediv1  10186  lt2mul2div  10200  lerec  10206  lediv2  10214  le2msq  10224  suprleub  10286  infmrgelb  10302  ofsubeq0  10311  ofsubge0  10313  avgle1  10556  avgle2  10557  cnref1o  10978  xleneg  11180  xltadd1  11211  xsubge0  11216  xposdif  11217  xltmul1  11247  supxrleub  11281  infmxrgelb  11289  iooneg  11397  iccneg  11398  iccsplit  11410  iccshftr  11411  iccshftl  11413  iccdil  11415  icccntr  11417  fzsplit2  11466  fzaddel  11485  fzrev  11511  elfzo  11547  fzon  11563  elfzom1b  11618  negmod0  11708  leexp2  11910  ltexp2r  11912  repswsymball  12409  repswsymballbi  12410  cjreb  12604  sqrlt  12743  limsuplt  12949  o1lo1  13007  rlimresb  13035  lo1eq  13038  rlimeq  13039  o1eq  13040  isercoll  13137  efle  13394  tanaddlem  13442  nndivdvds  13533  moddvds  13534  oddm1even  13585  bitsp1  13619  sadcaddlem  13645  sadadd  13655  sadass  13659  bitsshft  13663  smuval2  13670  smumul  13681  dvdssq  13736  phiprmpw  13843  eulerthlem2  13849  odzdvds  13859  pc2dvds  13937  1arith  13980  imasleval  14471  mreacs  14588  catpropd  14640  oppcsect  14704  funcres2b  14799  fthsect  14827  fthinv  14828  fucsect  14874  fucinv  14875  latnlemlt  15246  latnle  15247  ipole  15320  ipolt  15321  issubg3  15690  eqgid  15724  resghm2b  15756  conjghm  15768  gastacos  15819  resscntz  15840  cntzrec  15842  oppgsubm  15868  oppgsubg  15869  sylow3lem6  16122  lsmcom2  16145  lsmass  16158  lsmcomx  16329  subgdmdprd  16519  opprsubrg  16864  lsslss  17019  lbspropd  17157  islbs2  17212  rspsn  17313  psrbagconf1o  17421  gsumbagdiaglem  17422  mplmonmul  17520  prmirred  17894  prmirredOLD  17897  znfld  17968  lindfmm  18231  lindsmm  18232  lsslindf  18234  lsslinds  18235  islindf4  18242  basdif0  18533  neiptopreu  18712  neitr  18759  restlp  18762  cnrest2  18865  cnprest  18868  cnprest2  18869  lmss  18877  lmff  18880  ist1-2  18926  lpcls  18943  perfcls  18944  cmpfi  18986  hauseqlcld  19194  txlm  19196  txkgen  19200  xkopt  19203  idqtop  19254  tgqtop  19260  qtopcn  19262  uffix  19469  fmco  19509  flimrest  19531  lmflf  19553  txflf  19554  fclsrest  19572  cnpfcf  19589  tsmsgsum  19684  tsmsgsumOLD  19687  tsmsresOLD  19692  tsmsres  19693  tsmsf1o  19694  fmucndlem  19841  ismet2  19883  imasf1oxmet  19925  blres  19981  xmetec  19984  imasf1obl  20038  imasf1oxms  20039  prdsbl  20041  stdbdbl  20067  metrest  20074  metustsymOLD  20111  metustsym  20112  blval2  20125  metuel2  20129  tngngp  20215  cnbl0  20328  cnblcld  20329  bl2ioo  20344  cncfcnvcn  20472  iihalf2  20480  icoopnst  20486  iocopnst  20487  icopnfcnv  20489  icopnfhmeo  20490  cphorthcom  20694  caucfil  20769  lmclim  20788  cmsss  20836  rrxmet  20882  volsup  21012  dyaddisjlem  21050  mbfeqalem  21095  mbfeqa  21096  mbfmulc2lem  21100  mbfmax  21102  mbfposr  21105  ismbf3d  21107  mbfimaopnlem  21108  mbfaddlem  21113  mbfsup  21117  mbfinf  21118  0plef  21125  0pledm  21126  i1fmulclem  21155  i1fres  21158  i1fpos  21159  itg1climres  21167  mbfi1fseqlem4  21171  itg2mulclem  21199  itg2monolem1  21203  itg2cnlem1  21214  iblre  21246  iblcn  21251  itgeqa  21266  ellimc2  21327  limcflf  21331  dvreslem  21359  lhop1  21461  ply1remlem  21609  fta1glem2  21613  ofmulrt  21723  plydiveu  21739  plyremlem  21745  quotcan  21750  ulmres  21828  cos11  21964  logleb  22027  argrege0  22035  logdivle  22046  efopn  22078  logccv  22083  cxplt  22114  cxple  22115  cxple2  22117  cxplt2  22118  cxplt3  22120  cxple3  22121  angrtmuld  22179  quad2  22209  atans2  22301  rlimcnp  22334  rlimcnp2  22335  rlimcxp  22342  sqff1o  22495  fsumvma2  22528  dchrptlem2  22579  lgsdilem  22636  lgsne0  22647  lgsqr  22660  lgsquadlem1  22668  lgsquadlem2  22669  m1lgs  22676  dchrisum0lem1  22740  padicabv  22854  trgcgrg  22942  colcom  22966  colrot1  22967  lncom  23000  lnrot2  23002  israg  23056  colinearalglem2  23104  axcgrid  23113  uhgraeq12d  23192  usgraeq12d  23235  nbgrasym  23299  cusgrauvtxb  23355  eupath2lem3  23551  rngosn3  23864  nvsubsub23  23993  nmorepnf  24119  blocnilem  24155  ubthlem1  24222  shscom  24673  pjpreeq  24752  spansncol  24922  cmcm2  24970  hodsi  25130  nmoprepnf  25222  nmfnrepnf  25235  pjssposi  25527  cvcon3  25639  mdsymlem8  25765  dmdsym  25768  disjunsn  25887  unipreima  25912  fmptcof2  25930  1stpreima  25952  fpwrelmapffslem  25983  nndiffz1  26026  metider  26273  pstmxmet  26276  xrge0iifiso  26317  logblt  26417  indpi1  26430  indf1ofs  26434  aean  26612  brfae  26616  signsply0  26904  signsvfn  26935  subfacp1lem3  27022  subfacp1lem5  27024  opelco3  27540  predfz  27615  sscoid  27895  cgrcomr  27979  ofscom  27989  cgr3permute3  28029  cgr3permute1  28030  cgr3com  28035  colinearperm1  28044  colinearperm3  28045  outsideofcom  28110  wl-equsald  28319  wl-sbcom3  28364  heicant  28379  itg2addnclem2  28397  ftc1anclem1  28420  ftc1anclem5  28424  ftc1anclem6  28425  areacirclem5  28441  areacirc  28442  opnbnd  28473  filnetlem4  28555  caures  28609  cnpwstotbnd  28649  ismtyima  28655  rrnmet  28681  reheibor  28691  lzenom  29061  rmxycomplete  29211  fzneg  29278  modabsdifz  29287  jm2.19  29295  pw2f1ocnv  29339  caofcan  29550  rfcnpre1  29694  rfcnpre2  29706  pr1eqbg  30074  usg2wlkeq  30242  clwlkisclwwlk  30404  usg2spot2nb  30611  lco0  30850  lindslininds  30887  lcvbr  32506  lkrsc  32582  lshpkrlem1  32595  opltcon3b  32689  cmt2N  32735  cmt3N  32736  cvrcon3b  32762  cvrcmp2  32769  cvlexchb2  32816  cvlatexchb2  32820  2llnmj  33044  4atlem3  33080  4atlem9  33087  4atlem10a  33088  4atlem11a  33091  4atlem12a  33094  4at2  33098  2lplnmj  33106  llnexchb2  33353  lautlt  33575  lautcvr  33576  lautco  33581  ltrnatb  33621  ltrneq2  33632  cdlemefrs29pre00  33879  cdlemefrs29cpre1  33882  cdleme32fva  33921  dibglbN  34651  dochsncom  34867  dochkrsat  34940  lspindp5  35255  mapdh8ab  35262  hdmapip0com  35405