Theorem 3bitr4d 310

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	⊢ (𝜑 → (𝜓 ↔ 𝜒))
3bitr4d.2	⊢ (𝜑 → (𝜃 ↔ 𝜓))
3bitr4d.3	⊢ (𝜑 → (𝜏 ↔ 𝜒))

Assertion

Ref	Expression
3bitr4d	⊢ (𝜑 → (𝜃 ↔ 𝜏))

Proof of Theorem 3bitr4d

Step	Hyp	Ref	Expression
1		3bitr4d.2	. 2 ⊢ (𝜑 → (𝜃 ↔ 𝜓))
2		3bitr4d.1	. . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
3		3bitr4d.3	. . 3 ⊢ (𝜑 → (𝜏 ↔ 𝜒))
4	2, 3	bitr4d 281	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜏))
5	1, 4	bitrd 278	1 ⊢ (𝜑 → (𝜃 ↔ 𝜏))

Syntax hints:   → wi 4   ↔ wb 205

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 206

This theorem is referenced by:  pr1eqbg  4784  fvopab3g  6852  fvimacnvALT  6916  respreima  6925  fmptco  6983  fnnfpeq0  7032  cocan1  7143  cocan2  7144  ordsucelsuc  7644  ordsucsssuc  7645  fnsuppres  7978  smoword  8168  oaword  8342  omword  8363  om00el  8369  oeword  8383  nnaword  8420  nnmword  8426  swoer  8486  erth  8505  brecop  8557  eceqoveq  8569  xpdom2  8807  pw2f1olem  8816  ixpfi2  9047  cantnfrescl  9364  rankr1bg  9492  r1pwcl  9536  fseqenlem1  9711  alephord3  9765  alephdom2  9774  engch  10315  fpwwe2lem6  10323  fpwwe2lem8  10325  ltexpi  10589  ltapi  10590  ltmpi  10591  ltsonq  10656  ltmnq  10659  1idpr  10716  addcanpr  10733  axpre-ltadd  10854  axlttri  10977  subsub23  11156  leadd1  11373  ltsub1  11401  ltsub2  11402  leord1  11432  eqord1  11433  lemul1  11757  lediv1  11770  lt2mul2div  11783  lerec  11788  lediv2  11795  le2msq  11805  suprleub  11871  infregelb  11889  ofsubeq0  11900  ofsubge0  11902  avgle1  12143  avgle2  12144  cnref1o  12654  xleneg  12881  xnn0lem1lt  12907  xltadd1  12919  xsubge0  12924  xposdif  12925  xltmul1  12955  supxrleub  12989  infxrgelb  12998  iooneg  13132  iccneg  13133  iccsplit  13146  iccshftr  13147  iccshftl  13149  iccdil  13151  icccntr  13153  fzsplit2  13210  fzaddel  13219  fzrev  13248  predfz  13310  elfzo  13318  nelfzo  13321  fzon  13336  elfzom1b  13414  negmod0  13526  leexp2  13817  ltexp2r  13819  repswsymball  14420  repswsymballbi  14421  cjreb  14762  sqrtlt  14901  limsuplt  15116  o1lo1  15174  rlimresb  15202  lo1eq  15205  rlimeq  15206  o1eq  15207  isercoll  15307  efle  15755  tanaddlem  15803  nndivdvds  15900  moddvds  15902  modmulconst  15925  oddm1even  15980  ltoddhalfle  15998  bitsp1  16066  sadcaddlem  16092  sadadd  16102  sadass  16106  bitsshft  16110  smuval2  16117  smumul  16128  dvdssq  16200  phiprmpw  16405  eulerthlem2  16411  odzdvds  16424  pc2dvds  16508  1arith  16556  imasleval  17169  mreacs  17284  catpropd  17335  oppcsect  17407  funcres2b  17528  fthsect  17557  fthinv  17558  fucsect  17606  fucinv  17607  latnlemlt  18105  latnle  18106  ipole  18167  ipolt  18168  issubg3  18688  eqgid  18723  resghm2b  18767  conjghm  18780  gastacos  18831  resscntz  18853  cntzrec  18855  oppgsubm  18884  oppgsubg  18885  sylow3lem6  19152  lsmcom2  19175  lsmass  19190  ablsubsub23  19341  lsmcomx  19372  subgdmdprd  19552  opprsubrg  19960  lsslss  20138  lbspropd  20276  islbs2  20331  rspsn  20438  prmirred  20608  znfld  20680  lindfmm  20944  lindsmm  20945  lsslindf  20947  lsslinds  20948  islindf4  20955  psrbagconf1o  21049  psrbagconf1oOLD  21050  gsumbagdiaglemOLD  21051  gsumbagdiaglem  21054  mplmonmul  21147  basdif0  22011  neiptopreu  22192  neitr  22239  restlp  22242  cnrest2  22345  cnprest  22348  cnprest2  22349  lmss  22357  lmff  22360  ist1-2  22406  lpcls  22423  perfcls  22424  cmpfi  22467  hauseqlcld  22705  txlm  22707  txkgen  22711  xkopt  22714  idqtop  22765  tgqtop  22771  qtopcn  22773  uffix  22980  fmco  23020  flimrest  23042  lmflf  23064  txflf  23065  fclsrest  23083  cnpfcf  23100  tsmsgsum  23198  tsmsres  23203  tsmsf1o  23204  fmucndlem  23351  ismet2  23394  imasf1oxmet  23436  blres  23492  xmetec  23495  imasf1obl  23550  imasf1oxms  23551  prdsbl  23553  stdbdbl  23579  metrest  23586  metustsym  23617  blval2  23624  metuel2  23627  tngngp  23724  cnbl0  23843  cnblcld  23844  bl2ioo  23861  cncfcnvcn  23994  iihalf2  24002  icoopnst  24008  iocopnst  24009  icopnfcnv  24011  icopnfhmeo  24012  cphorthcom  24270  caucfil  24352  lmclim  24372  cmsss  24420  rrxmet  24477  volsup  24625  dyaddisjlem  24664  mbfeqalem1  24710  mbfeqalem2  24711  mbfeqa  24712  mbfmulc2lem  24716  mbfmax  24718  mbfposr  24721  ismbf3d  24723  mbfimaopnlem  24724  mbfaddlem  24729  mbfsup  24733  mbfinf  24734  0plef  24741  0pledm  24742  i1fmulclem  24772  i1fres  24775  i1fpos  24776  itg1climres  24784  mbfi1fseqlem4  24788  itg2mulclem  24816  itg2monolem1  24820  itg2cnlem1  24831  iblre  24863  iblcn  24868  itgeqa  24883  ellimc2  24946  limcflf  24950  dvreslem  24978  lhop1  25083  ply1remlem  25232  fta1glem2  25236  ofmulrt  25347  plydiveu  25363  plyremlem  25369  quotcan  25374  ulmres  25452  cos11  25594  logleb  25663  argrege0  25671  logdivle  25682  efopn  25718  logccv  25723  cxplt  25754  cxple  25755  cxple2  25757  cxplt2  25758  cxplt3  25760  cxple3  25761  logbleb  25838  logblt  25839  angrtmuld  25863  quad2  25894  atans2  25986  rlimcnp  26020  rlimcnp2  26021  rlimcxp  26028  sqff1o  26236  fsumvma2  26267  dchrptlem2  26318  lgsdilem  26377  lgsne0  26388  lgsqr  26404  lgsquadlem1  26433  lgsquadlem2  26434  m1lgs  26441  2lgslem1a  26444  2lgs  26460  dchrisum0lem1  26569  padicabv  26683  trgcgrg  26780  colcom  26823  colrot1  26824  ishlg  26867  hlcomb  26868  hlbtwn  26876  lncom  26887  lnrot2  26889  israg  26962  perpcom  26978  hpgcom  27032  colopp  27034  iscgra  27074  isinag  27103  colinearalglem2  27178  axcgrid  27187  uvtx01vtx  27667  iscplgredg  27687  rgrusgrprc  27859  uspgr2wlkeq  27915  clwlkclwwlk  28267  eupth2lem3lem6  28498  fusgr2wsp2nb  28599  nmorepnf  29031  blocnilem  29067  ubthlem1  29133  shscom  29582  pjpreeq  29661  spansncol  29831  cmcm2  29879  hodsi  30038  nmoprepnf  30130  nmfnrepnf  30143  pjssposi  30435  cvcon3  30547  mdsymlem8  30673  dmdsym  30676  disjunsn  30834  fimarab  30881  unipreima  30882  fmptcof2  30896  ressupprn  30926  1stpreima  30941  fpwrelmapffslem  30969  infxrge0gelb  30991  nndiffz1  31009  mgccnv  31179  pwrssmgc  31180  cntzun  31222  isinftm  31337  qusxpid  31461  lindfpropd  31478  lindspropd  31479  lsmssass  31492  nsgmgc  31499  finexttrb  31639  ist0cld  31685  metidv  31744  metider  31746  pstmxmet  31749  xrge0iifiso  31787  indpi1  31888  prodindf  31891  indf1ofs  31894  aean  32112  brfae  32116  signsply0  32430  signsvfn  32461  reprinrn  32498  subfacp1lem3  33044  subfacp1lem5  33046  fmlafvel  33247  eldifsucnn  33597  opelco3  33655  ttrclselem2  33712  naddss1  33768  nosupinfsep  33862  oldlim  33996  newbday  34009  sscoid  34142  cgrcomr  34226  ofscom  34236  cgr3permute3  34276  cgr3permute1  34277  cgr3com  34282  colinearperm1  34291  colinearperm3  34292  outsideofcom  34357  opnbnd  34441  filnetlem4  34497  finxpsuclem  35495  wl-equsald  35625  lindsadd  35697  poimirlem23  35727  broucube  35738  heicant  35739  itg2addnclem2  35756  ftc1anclem1  35777  ftc1anclem5  35781  ftc1anclem6  35782  areacirclem5  35796  areacirc  35797  caures  35845  cnpwstotbnd  35882  ismtyima  35888  rrnmet  35914  reheibor  35924  rngosn3  36009  brcosscnvcoss  36484  br1cosscnvxrn  36519  eqvrelth  36651  lcvbr  36962  lkrsc  37038  lshpkrlem1  37051  opltcon3b  37145  cmt2N  37191  cmt3N  37192  cvrcon3b  37218  cvrcmp2  37225  cvlexchb2  37272  cvlatexchb2  37276  2llnmj  37501  4atlem3  37537  4atlem9  37544  4atlem10a  37545  4atlem11a  37548  4atlem12a  37551  4at2  37555  2lplnmj  37563  llnexchb2  37810  lautlt  38032  lautcvr  38033  lautco  38038  ltrnatb  38078  ltrneq2  38089  cdlemefrs29pre00  38336  cdlemefrs29cpre1  38339  cdleme32fva  38378  dibglbN  39107  dochsncom  39323  dochkrsat  39396  lspindp5  39711  mapdh8ab  39718  hdmapip0com  39858  fsuppind  40202  dvdsexpb  40263  sn-ltmul2d  40352  prjsprellsp  40371  lzenom  40508  rmxycomplete  40655  fzneg  40720  modabsdifz  40724  jm2.19  40731  pw2f1ocnv  40775  sqrtcvallem1  41128  brtrclfv2  41224  rfovcnvf1od  41501  ntrclsfveq1  41559  ntrclsiso  41566  k0004lem2  41647  caofcan  41830  rfcnpre1  42451  rfcnpre2  42463  ellimcabssub0  43048  liminfpnfuz  43247  xlimpnfxnegmnf2  43289  fperdvper  43350  vonvolmbl  44089  readdcnnred  44683  resubcnnred  44684  cndivrenred  44686  requad2  44963  mgmpropd  45217  lco0  45656  lindslininds  45693  ltsubaddb  45743  ltsubsubb  45744  ltsubadd2b  45745  elbigolo1  45791  dig2bits  45848  rrx2pnedifcoorneorr  45951  mofeu  46063  sepnsepo  46105  lubeldm2d  46140  glbeldm2d  46141  thincsect2  46227  thinccic  46230  postcposALT  46248