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  2174  r19.12sn  4093  sbcbr  4500  fvopab3g  5946  fvimacnvALT  6000  respreima  6010  fmptco  6054  fnnfpeq0  6092  fnsuppresOLD  6121  cocan1  6182  cocan2  6183  ordsucelsuc  6641  ordsucsssuc  6642  fnsuppres  6927  smoword  7037  oaword  7198  omword  7219  om00el  7225  oeword  7239  nnaword  7276  nnmword  7282  swoer  7339  erth  7356  brecop  7404  eceqoveq  7416  xpdom2  7612  pw2f1olem  7621  omsucdomOLD  7713  fisucdomOLD  7723  ixpfi2  7818  wemapso2lem  7978  cantnfrescl  8095  rankr1bg  8221  r1pwcl  8265  fseqenlem1  8405  alephord3  8459  alephdom2  8468  engch  9006  fpwwe2lem7  9014  fpwwe2lem9  9016  ltexpi  9280  ltapi  9281  ltmpi  9282  ltsonq  9347  ltmnq  9350  1idpr  9407  addcanpr  9424  axpre-ltadd  9544  axlttri  9656  subsub23  9825  leadd1  10020  ltsub1  10048  ltsub2  10049  leord1  10080  eqord1  10081  lemul1  10394  lediv1  10407  lt2mul2div  10421  lerec  10427  lediv2  10435  le2msq  10445  suprleub  10507  infmrgelb  10523  ofsubeq0  10533  ofsubge0  10535  avgle1  10778  avgle2  10779  cnref1o  11215  xleneg  11417  xltadd1  11448  xsubge0  11453  xposdif  11454  xltmul1  11484  supxrleub  11518  infmxrgelb  11526  iooneg  11640  iccneg  11641  iccsplit  11653  iccshftr  11654  iccshftl  11656  iccdil  11658  icccntr  11660  fzsplit2  11710  fzaddel  11718  fzrev  11742  elfzo  11799  fzon  11815  elfzom1b  11879  negmod0  11972  leexp2  12188  ltexp2r  12190  repswsymball  12714  repswsymballbi  12715  cjreb  12919  sqrtlt  13058  limsuplt  13265  o1lo1  13323  rlimresb  13351  lo1eq  13354  rlimeq  13355  o1eq  13356  isercoll  13453  efle  13714  tanaddlem  13762  nndivdvds  13853  moddvds  13854  oddm1even  13906  bitsp1  13940  sadcaddlem  13966  sadadd  13976  sadass  13980  bitsshft  13984  smuval2  13991  smumul  14002  dvdssq  14057  phiprmpw  14165  eulerthlem2  14171  odzdvds  14181  pc2dvds  14261  1arith  14304  imasleval  14796  mreacs  14913  catpropd  14965  oppcsect  15029  funcres2b  15124  fthsect  15152  fthinv  15153  fucsect  15199  fucinv  15200  latnlemlt  15571  latnle  15572  ipole  15645  ipolt  15646  issubg3  16024  eqgid  16058  resghm2b  16090  conjghm  16102  gastacos  16153  resscntz  16174  cntzrec  16176  oppgsubm  16202  oppgsubg  16203  sylow3lem6  16458  lsmcom2  16481  lsmass  16494  lsmcomx  16665  subgdmdprd  16883  opprsubrg  17250  lsslss  17407  lbspropd  17545  islbs2  17600  rspsn  17701  psrbagconf1o  17825  gsumbagdiaglem  17826  mplmonmul  17925  prmirred  18320  prmirredOLD  18323  znfld  18394  lindfmm  18657  lindsmm  18658  lsslindf  18660  lsslinds  18661  islindf4  18668  basdif0  19249  neiptopreu  19428  neitr  19475  restlp  19478  cnrest2  19581  cnprest  19584  cnprest2  19585  lmss  19593  lmff  19596  ist1-2  19642  lpcls  19659  perfcls  19660  cmpfi  19702  hauseqlcld  19910  txlm  19912  txkgen  19916  xkopt  19919  idqtop  19970  tgqtop  19976  qtopcn  19978  uffix  20185  fmco  20225  flimrest  20247  lmflf  20269  txflf  20270  fclsrest  20288  cnpfcf  20305  tsmsgsum  20400  tsmsgsumOLD  20403  tsmsresOLD  20408  tsmsres  20409  tsmsf1o  20410  fmucndlem  20557  ismet2  20599  imasf1oxmet  20641  blres  20697  xmetec  20700  imasf1obl  20754  imasf1oxms  20755  prdsbl  20757  stdbdbl  20783  metrest  20790  metustsymOLD  20827  metustsym  20828  blval2  20841  metuel2  20845  tngngp  20931  cnbl0  21044  cnblcld  21045  bl2ioo  21060  cncfcnvcn  21188  iihalf2  21196  icoopnst  21202  iocopnst  21203  icopnfcnv  21205  icopnfhmeo  21206  cphorthcom  21410  caucfil  21485  lmclim  21504  cmsss  21552  rrxmet  21598  volsup  21729  dyaddisjlem  21767  mbfeqalem  21812  mbfeqa  21813  mbfmulc2lem  21817  mbfmax  21819  mbfposr  21822  ismbf3d  21824  mbfimaopnlem  21825  mbfaddlem  21830  mbfsup  21834  mbfinf  21835  0plef  21842  0pledm  21843  i1fmulclem  21872  i1fres  21875  i1fpos  21876  itg1climres  21884  mbfi1fseqlem4  21888  itg2mulclem  21916  itg2monolem1  21920  itg2cnlem1  21931  iblre  21963  iblcn  21968  itgeqa  21983  ellimc2  22044  limcflf  22048  dvreslem  22076  lhop1  22178  ply1remlem  22326  fta1glem2  22330  ofmulrt  22440  plydiveu  22456  plyremlem  22462  quotcan  22467  ulmres  22545  cos11  22681  logleb  22744  argrege0  22752  logdivle  22763  efopn  22795  logccv  22800  cxplt  22831  cxple  22832  cxple2  22834  cxplt2  22835  cxplt3  22837  cxple3  22838  angrtmuld  22896  quad2  22926  atans2  23018  rlimcnp  23051  rlimcnp2  23052  rlimcxp  23059  sqff1o  23212  fsumvma2  23245  dchrptlem2  23296  lgsdilem  23353  lgsne0  23364  lgsqr  23377  lgsquadlem1  23385  lgsquadlem2  23386  m1lgs  23393  dchrisum0lem1  23457  padicabv  23571  trgcgrg  23662  colcom  23701  colrot1  23702  lncom  23744  lnrot2  23746  israg  23810  perpcom  23826  colinearalglem2  23914  axcgrid  23923  uhgraeq12d  24011  usgraeq12d  24066  nbgrasym  24143  cusgrauvtxb  24200  usg2wlkeq  24412  clwlkisclwwlk  24493  eupath2lem3  24683  usg2spot2nb  24770  rngosn3  25132  nvsubsub23  25261  nmorepnf  25387  blocnilem  25423  ubthlem1  25490  shscom  25941  pjpreeq  26020  spansncol  26190  cmcm2  26238  hodsi  26398  nmoprepnf  26490  nmfnrepnf  26503  pjssposi  26795  cvcon3  26907  mdsymlem8  27033  dmdsym  27036  disjunsn  27154  unipreima  27184  fmptcof2  27202  1stpreima  27224  fpwrelmapffslem  27255  nndiffz1  27292  metider  27537  pstmxmet  27540  xrge0iifiso  27581  logblt  27690  indpi1  27703  indf1ofs  27707  aean  27884  brfae  27888  signsply0  28176  signsvfn  28207  subfacp1lem3  28294  subfacp1lem5  28296  opelco3  28813  predfz  28888  sscoid  29168  cgrcomr  29252  ofscom  29262  cgr3permute3  29302  cgr3permute1  29303  cgr3com  29308  colinearperm1  29317  colinearperm3  29318  outsideofcom  29383  wl-equsald  29597  wl-sbcom3  29640  heicant  29654  itg2addnclem2  29672  ftc1anclem1  29695  ftc1anclem5  29699  ftc1anclem6  29700  areacirclem5  29716  areacirc  29717  opnbnd  29748  filnetlem4  29830  caures  29884  cnpwstotbnd  29924  ismtyima  29930  rrnmet  29956  reheibor  29966  lzenom  30335  rmxycomplete  30485  fzneg  30552  modabsdifz  30559  jm2.19  30567  pw2f1ocnv  30611  caofcan  30856  rfcnpre1  31000  rfcnpre2  31012  pr1eqbg  31792  isfusgracl  31921  isfusgraclALT  31923  fusgraimpclALT2  31926  lco0  32127  lindslininds  32164  lcvbr  33836  lkrsc  33912  lshpkrlem1  33925  opltcon3b  34019  cmt2N  34065  cmt3N  34066  cvrcon3b  34092  cvrcmp2  34099  cvlexchb2  34146  cvlatexchb2  34150  2llnmj  34374  4atlem3  34410  4atlem9  34417  4atlem10a  34418  4atlem11a  34421  4atlem12a  34424  4at2  34428  2lplnmj  34436  llnexchb2  34683  lautlt  34905  lautcvr  34906  lautco  34911  ltrnatb  34951  ltrneq2  34962  cdlemefrs29pre00  35209  cdlemefrs29cpre1  35212  cdleme32fva  35251  dibglbN  35981  dochsncom  36197  dochkrsat  36270  lspindp5  36585  mapdh8ab  36592  hdmapip0com  36735