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  4010  sbcbr  4419  fvopab3g  5853  fvimacnvALT  5908  respreima  5918  fmptco  5966  fnnfpeq0  6004  fnsuppresOLD  6033  cocan1  6095  cocan2  6096  ordsucelsuc  6556  ordsucsssuc  6557  fnsuppres  6845  smoword  6955  oaword  7116  omword  7137  om00el  7143  oeword  7157  nnaword  7194  nnmword  7200  swoer  7257  erth  7274  brecop  7322  eceqoveq  7334  xpdom2  7531  pw2f1olem  7540  ixpfi2  7733  wemapso2lem  7893  cantnfrescl  8008  rankr1bg  8134  r1pwcl  8178  fseqenlem1  8318  alephord3  8372  alephdom2  8381  engch  8917  fpwwe2lem7  8925  fpwwe2lem9  8927  ltexpi  9191  ltapi  9192  ltmpi  9193  ltsonq  9258  ltmnq  9261  1idpr  9318  addcanpr  9335  axpre-ltadd  9455  axlttri  9567  subsub23  9738  leadd1  9938  ltsub1  9966  ltsub2  9967  leord1  9997  eqord1  9998  lemul1  10311  lediv1  10324  lt2mul2div  10337  lerec  10343  lediv2  10351  le2msq  10361  suprleub  10423  infmrgelb  10439  ofsubeq0  10449  ofsubge0  10451  avgle1  10695  avgle2  10696  cnref1o  11134  xleneg  11338  xltadd1  11369  xsubge0  11374  xposdif  11375  xltmul1  11405  supxrleub  11439  infmxrgelb  11447  iooneg  11561  iccneg  11562  iccsplit  11574  iccshftr  11575  iccshftl  11577  iccdil  11579  icccntr  11581  fzsplit2  11631  fzaddel  11640  fzrev  11664  elfzo  11724  nelfzo  11727  fzon  11741  elfzom1b  11810  negmod0  11905  leexp2  12123  ltexp2r  12125  repswsymball  12662  repswsymballbi  12663  cjreb  12958  sqrtlt  13097  limsuplt  13304  o1lo1  13362  rlimresb  13390  lo1eq  13393  rlimeq  13394  o1eq  13395  isercoll  13492  efle  13855  tanaddlem  13903  nndivdvds  13994  moddvds  13995  oddm1even  14049  bitsp1  14083  sadcaddlem  14109  sadadd  14119  sadass  14123  bitsshft  14127  smuval2  14134  smumul  14145  dvdssq  14200  phiprmpw  14308  eulerthlem2  14314  odzdvds  14324  pc2dvds  14404  1arith  14447  imasleval  14948  mreacs  15065  catpropd  15115  oppcsect  15184  funcres2b  15303  fthsect  15331  fthinv  15332  fucsect  15378  fucinv  15379  latnlemlt  15831  latnle  15832  ipole  15905  ipolt  15906  issubg3  16336  eqgid  16370  resghm2b  16402  conjghm  16414  gastacos  16465  resscntz  16486  cntzrec  16488  oppgsubm  16514  oppgsubg  16515  sylow3lem6  16769  lsmcom2  16792  lsmass  16805  lsmcomx  16979  subgdmdprd  17194  opprsubrg  17563  lsslss  17720  lbspropd  17858  islbs2  17913  rspsn  18015  psrbagconf1o  18139  gsumbagdiaglem  18140  mplmonmul  18239  prmirred  18625  znfld  18690  lindfmm  18947  lindsmm  18948  lsslindf  18950  lsslinds  18951  islindf4  18958  basdif0  19539  neiptopreu  19720  neitr  19767  restlp  19770  cnrest2  19873  cnprest  19876  cnprest2  19877  lmss  19885  lmff  19888  ist1-2  19934  lpcls  19951  perfcls  19952  cmpfi  19994  hauseqlcld  20232  txlm  20234  txkgen  20238  xkopt  20241  idqtop  20292  tgqtop  20298  qtopcn  20300  uffix  20507  fmco  20547  flimrest  20569  lmflf  20591  txflf  20592  fclsrest  20610  cnpfcf  20627  tsmsgsum  20722  tsmsgsumOLD  20725  tsmsresOLD  20730  tsmsres  20731  tsmsf1o  20732  fmucndlem  20879  ismet2  20921  imasf1oxmet  20963  blres  21019  xmetec  21022  imasf1obl  21076  imasf1oxms  21077  prdsbl  21079  stdbdbl  21105  metrest  21112  metustsymOLD  21149  metustsym  21150  blval2  21163  metuel2  21167  tngngp  21253  cnbl0  21366  cnblcld  21367  bl2ioo  21382  cncfcnvcn  21510  iihalf2  21518  icoopnst  21524  iocopnst  21525  icopnfcnv  21527  icopnfhmeo  21528  cphorthcom  21732  caucfil  21807  lmclim  21826  cmsss  21874  rrxmet  21920  volsup  22051  dyaddisjlem  22089  mbfeqalem  22134  mbfeqa  22135  mbfmulc2lem  22139  mbfmax  22141  mbfposr  22144  ismbf3d  22146  mbfimaopnlem  22147  mbfaddlem  22152  mbfsup  22156  mbfinf  22157  0plef  22164  0pledm  22165  i1fmulclem  22194  i1fres  22197  i1fpos  22198  itg1climres  22206  mbfi1fseqlem4  22210  itg2mulclem  22238  itg2monolem1  22242  itg2cnlem1  22253  iblre  22285  iblcn  22290  itgeqa  22305  ellimc2  22366  limcflf  22370  dvreslem  22398  lhop1  22500  ply1remlem  22648  fta1glem2  22652  ofmulrt  22763  plydiveu  22779  plyremlem  22785  quotcan  22790  ulmres  22868  cos11  23005  logleb  23075  argrege0  23083  logdivle  23094  efopn  23126  logccv  23131  cxplt  23162  cxple  23163  cxple2  23165  cxplt2  23166  cxplt3  23168  cxple3  23169  logbleb  23241  logblt  23242  angrtmuld  23258  quad2  23286  atans2  23378  rlimcnp  23412  rlimcnp2  23413  rlimcxp  23420  sqff1o  23573  fsumvma2  23606  dchrptlem2  23657  lgsdilem  23714  lgsne0  23725  lgsqr  23738  lgsquadlem1  23746  lgsquadlem2  23747  m1lgs  23754  dchrisum0lem1  23818  padicabv  23932  trgcgrg  24026  colcom  24065  colrot1  24066  ishlg  24106  hlcomb  24107  hlbtwn  24115  lncom  24122  lnrot2  24124  israg  24194  perpcom  24210  hpgcom  24256  iscgra  24289  colinearalglem2  24331  axcgrid  24340  uhgraeq12d  24428  usgraeq12d  24483  nbgrasym  24560  cusgrauvtxb  24617  usg2wlkeq  24829  clwlkisclwwlk  24910  eupath2lem3  25100  usg2spot2nb  25186  rngosn3  25545  nvsubsub23  25674  nmorepnf  25800  blocnilem  25836  ubthlem1  25903  shscom  26354  pjpreeq  26433  spansncol  26603  cmcm2  26651  hodsi  26810  nmoprepnf  26902  nmfnrepnf  26915  pjssposi  27207  cvcon3  27319  mdsymlem8  27445  dmdsym  27448  disjunsn  27583  fimarab  27623  unipreima  27624  fmptcof2  27643  1stpreima  27672  fpwrelmapffslem  27705  nndiffz1  27749  isinftm  27878  metidv  28025  metider  28027  pstmxmet  28030  xrge0iifiso  28071  indpi1  28170  indf1ofs  28174  aean  28372  brfae  28376  signsply0  28691  signsvfn  28722  subfacp1lem3  28815  subfacp1lem5  28817  opelco3  29373  predfz  29448  sscoid  29716  cgrcomr  29800  ofscom  29810  cgr3permute3  29850  cgr3permute1  29851  cgr3com  29856  colinearperm1  29865  colinearperm3  29866  outsideofcom  29931  wl-equsald  30157  wl-sbcom3  30200  heicant  30214  itg2addnclem2  30233  ftc1anclem1  30256  ftc1anclem5  30260  ftc1anclem6  30261  areacirclem5  30277  areacirc  30278  opnbnd  30309  filnetlem4  30365  caures  30419  cnpwstotbnd  30459  ismtyima  30465  rrnmet  30491  reheibor  30501  lzenom  30868  rmxycomplete  31018  fzneg  31085  modabsdifz  31092  jm2.19  31101  pw2f1ocnv  31145  caofcan  31396  rfcnpre1  31561  rfcnpre2  31573  ellimcabssub0  31789  fperdvper  31881  pr1eqbg  32618  isfusgracl  32744  isfusgraclALT  32746  fusgraimpclALT2  32749  mgmpropd  32781  lco0  33228  lindslininds  33265  ltsubaddb  33319  ltsubsubb  33320  ltsubadd2b  33321  elbigolo1  33378  dig2bits  33435  lcvbr  35159  lkrsc  35235  lshpkrlem1  35248  opltcon3b  35342  cmt2N  35388  cmt3N  35389  cvrcon3b  35415  cvrcmp2  35422  cvlexchb2  35469  cvlatexchb2  35473  2llnmj  35697  4atlem3  35733  4atlem9  35740  4atlem10a  35741  4atlem11a  35744  4atlem12a  35747  4at2  35751  2lplnmj  35759  llnexchb2  36006  lautlt  36228  lautcvr  36229  lautco  36234  ltrnatb  36274  ltrneq2  36285  cdlemefrs29pre00  36534  cdlemefrs29cpre1  36537  cdleme32fva  36576  dibglbN  37306  dochsncom  37522  dochkrsat  37595  lspindp5  37910  mapdh8ab  37917  hdmapip0com  38060  brtrclfv2  38258