Theorem 3bitr4d 311

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 282	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜏))
5	1, 4	bitrd 279	1 ⊢ (𝜑 → (𝜃 ↔ 𝜏))

Syntax hints:   → wi 4   ↔ wb 206

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 207

This theorem is referenced by:  sbccomlem  3823  pr1eqbg  4811  unisucg  6391  fimarab  6901  fvopab3g  6929  fvimacnvALT  6995  respreima  7004  fmptco  7067  fnnfpeq0  7118  cocan1  7232  cocan2  7233  caofidlcan  7655  ordsucelsuc  7761  ordsucsssuc  7762  fnsuppres  8131  smoword  8296  oaword  8474  omword  8495  om00el  8501  oeword  8515  nnaword  8552  nnmword  8558  eldifsucnn  8589  naddss1  8614  naddunif  8618  swoer  8663  erth  8686  brecop  8744  eceqoveq  8756  xpdom2  8996  pw2f1olem  9005  ixpfi2  9259  cantnfrescl  9591  ttrclselem2  9641  rankr1bg  9718  r1pwcl  9762  fseqenlem1  9937  alephord3  9991  alephdom2  10000  engch  10541  fpwwe2lem6  10549  fpwwe2lem8  10551  ltexpi  10815  ltapi  10816  ltmpi  10817  ltsonq  10882  ltmnq  10885  1idpr  10942  addcanpr  10959  axpre-ltadd  11080  axlttri  11205  subsub23  11386  leadd1  11606  ltsub1  11634  ltsub2  11635  leord1  11665  eqord1  11666  lemul1  11994  lediv1  12008  lt2mul2div  12021  lerec  12026  lediv2  12033  le2msq  12043  suprleub  12109  infregelb  12127  ofsubeq0  12143  ofsubge0  12145  avgle1  12382  avgle2  12383  cnref1o  12904  xleneg  13138  xnn0lem1lt  13164  xltadd1  13176  xsubge0  13181  xposdif  13182  xltmul1  13212  supxrleub  13246  infxrgelb  13256  iooneg  13392  iccneg  13393  iccsplit  13406  iccshftr  13407  iccshftl  13409  iccdil  13411  icccntr  13413  fzsplit2  13470  fzaddel  13479  fzrev  13508  predfz  13574  elfzo  13582  nelfzo  13585  fzon  13601  elfzom1b  13687  negmod0  13800  leexp2  14096  ltexp2r  14098  repswsymball  14703  repswsymballbi  14704  cjreb  15048  sqrtlt  15186  limsuplt  15404  o1lo1  15462  rlimresb  15490  lo1eq  15493  rlimeq  15494  o1eq  15495  isercoll  15593  efle  16045  tanaddlem  16093  nndivdvds  16190  moddvds  16192  modmulconst  16217  oddm1even  16272  ltoddhalfle  16290  bitsp1  16360  sadcaddlem  16386  sadadd  16396  sadass  16400  bitsshft  16404  smuval2  16411  smumul  16422  dvdssq  16496  phiprmpw  16705  eulerthlem2  16711  odzdvds  16725  pc2dvds  16809  1arith  16857  imasleval  17463  mreacs  17582  catpropd  17633  oppcsect  17703  funcres2b  17822  fthsect  17852  fthinv  17853  fucsect  17900  fucinv  17901  latnlemlt  18396  latnle  18397  ipole  18458  ipolt  18459  mgmpropd  18543  issubg3  19041  eqgid  19077  resghm2b  19131  conjghm  19146  ghmqusker  19184  gastacos  19207  resscntz  19230  cntzrec  19233  oppgsubm  19259  oppgsubg  19260  sylow3lem6  19529  lsmcom2  19552  lsmass  19566  ablsubsub23  19721  lsmcomx  19753  subgdmdprd  19933  opprsubrng  20462  opprsubrg  20496  lsslss  20882  lbspropd  21021  islbs2  21079  rspsn  21258  prmirred  21399  znfld  21485  lindfmm  21752  lindsmm  21753  lsslindf  21755  lsslinds  21756  islindf4  21763  psrbagconf1o  21854  gsumbagdiaglem  21855  mplmonmul  21959  basdif0  22856  neiptopreu  23036  neitr  23083  restlp  23086  cnrest2  23189  cnprest  23192  cnprest2  23193  lmss  23201  lmff  23204  ist1-2  23250  lpcls  23267  perfcls  23268  cmpfi  23311  hauseqlcld  23549  txlm  23551  txkgen  23555  xkopt  23558  idqtop  23609  tgqtop  23615  qtopcn  23617  uffix  23824  fmco  23864  flimrest  23886  lmflf  23908  txflf  23909  fclsrest  23927  cnpfcf  23944  tsmsgsum  24042  tsmsres  24047  tsmsf1o  24048  fmucndlem  24194  ismet2  24237  imasf1oxmet  24279  blres  24335  xmetec  24338  imasf1obl  24392  imasf1oxms  24393  prdsbl  24395  stdbdbl  24421  metrest  24428  metustsym  24459  blval2  24466  metuel2  24469  tngngp  24558  cnbl0  24677  cnblcld  24678  bl2ioo  24696  cncfcnvcn  24835  iihalf2  24844  icoopnst  24852  iocopnst  24853  icopnfcnv  24856  icopnfhmeo  24857  cphorthcom  25117  caucfil  25199  lmclim  25219  cmsss  25267  rrxmet  25324  volsup  25473  dyaddisjlem  25512  mbfeqalem1  25558  mbfeqalem2  25559  mbfeqa  25560  mbfmulc2lem  25564  mbfmax  25566  mbfposr  25569  ismbf3d  25571  mbfimaopnlem  25572  mbfaddlem  25577  mbfsup  25581  mbfinf  25582  0plef  25589  0pledm  25590  i1fmulclem  25619  i1fres  25622  i1fpos  25623  itg1climres  25631  mbfi1fseqlem4  25635  itg2mulclem  25663  itg2monolem1  25667  itg2cnlem1  25678  iblre  25711  iblcn  25716  itgeqa  25731  ellimc2  25794  limcflf  25798  dvreslem  25826  lhop1  25935  r1pid2  26083  ply1remlem  26086  fta1glem2  26090  ofmulrt  26205  plydiveu  26222  plyremlem  26228  quotcan  26233  ulmres  26313  cos11  26458  logleb  26528  argrege0  26536  logdivle  26547  efopn  26583  logccv  26588  cxplt  26619  cxple  26620  cxple2  26622  cxplt2  26623  cxplt3  26625  cxple3  26626  recxpf1lem  26654  logbleb  26709  logblt  26710  angrtmuld  26734  quad2  26765  atans2  26857  rlimcnp  26891  rlimcnp2  26892  rlimcxp  26900  sqff1o  27108  fsumvma2  27141  dchrptlem2  27192  lgsdilem  27251  lgsne0  27262  lgsqr  27278  lgsquadlem1  27307  lgsquadlem2  27308  m1lgs  27315  2lgslem1a  27318  2lgs  27334  dchrisum0lem1  27443  padicabv  27557  nosupinfsep  27660  oldlim  27819  newbday  27834  slelss  27841  sltadd2  27921  sleneg  27975  sltsub2  28004  sltsubsubbd  28010  slesubsubbd  28013  slesubsub2bd  28014  slesubsub3bd  28015  slemul2d  28100  slemul1d  28101  sltmulneg1d  28102  n0subs2  28277  trgcgrg  28478  colcom  28521  colrot1  28522  ishlg  28565  hlcomb  28566  hlbtwn  28574  lncom  28585  lnrot2  28587  israg  28660  perpcom  28676  hpgcom  28730  colopp  28732  iscgra  28772  isinag  28801  colinearalglem2  28870  axcgrid  28879  uvtx01vtx  29360  iscplgredg  29380  rgrusgrprc  29553  uspgr2wlkeq  29609  dfpth2  29692  clwlkclwwlk  29964  eupth2lem3lem6  30195  fusgr2wsp2nb  30296  nmorepnf  30730  blocnilem  30766  ubthlem1  30832  shscom  31281  pjpreeq  31360  spansncol  31530  cmcm2  31578  hodsi  31737  nmoprepnf  31829  nmfnrepnf  31842  pjssposi  32134  cvcon3  32246  mdsymlem8  32372  dmdsym  32375  disjunsn  32556  unipreima  32600  fmptcof2  32614  fdifsupp  32641  ressupprn  32646  1stpreima  32663  fpwrelmapffslem  32688  infxrge0gelb  32722  nndiffz1  32742  indpi1  32816  prodindf  32819  indf1ofs  32822  mgccnv  32954  pwrssmgc  32955  gsumwrd2dccatlem  33032  cntzun  33034  cntrval2  33126  isinftm  33133  qusxpid  33310  lindfpropd  33329  lindspropd  33330  unitprodclb  33336  lsmssass  33349  nsgmgc  33359  crngmxidl  33416  opprqusdrng  33440  qsfld  33445  ply1dg1rt  33524  finexttrb  33636  algextdeglem7  33689  ist0cld  33799  metidv  33858  metider  33860  pstmxmet  33863  xrge0iifiso  33901  aean  34210  brfae  34214  signsply0  34518  signsvfn  34549  reprinrn  34585  subfacp1lem3  35154  subfacp1lem5  35156  fmlafvel  35357  opelco3  35747  sscoid  35886  cgrcomr  35970  ofscom  35980  cgr3permute3  36020  cgr3permute1  36021  cgr3com  36026  colinearperm1  36035  colinearperm3  36036  outsideofcom  36101  opnbnd  36298  filnetlem4  36354  finxpsuclem  37370  wl-equsald  37512  wl-equsaldv  37513  lindsadd  37592  poimirlem23  37622  broucube  37633  heicant  37634  itg2addnclem2  37651  ftc1anclem1  37672  ftc1anclem5  37676  ftc1anclem6  37677  areacirclem5  37691  areacirc  37692  caures  37739  cnpwstotbnd  37776  ismtyima  37782  rrnmet  37808  reheibor  37818  rngosn3  37903  brcosscnvcoss  38410  br1cosscnvxrn  38450  eqvrelth  38587  brpartspart  38750  lcvbr  38999  lkrsc  39075  lshpkrlem1  39088  opltcon3b  39182  cmt2N  39228  cmt3N  39229  cvrcon3b  39255  cvrcmp2  39262  cvlexchb2  39309  cvlatexchb2  39313  2llnmj  39539  4atlem3  39575  4atlem9  39582  4atlem10a  39583  4atlem11a  39586  4atlem12a  39589  4at2  39593  2lplnmj  39601  llnexchb2  39848  lautlt  40070  lautcvr  40071  lautco  40076  ltrnatb  40116  ltrneq2  40127  cdlemefrs29pre00  40374  cdlemefrs29cpre1  40377  cdleme32fva  40416  dibglbN  41145  dochsncom  41361  dochkrsat  41434  lspindp5  41749  mapdh8ab  41756  hdmapip0com  41896  dvdsexpb  42308  sn-ltmul2d  42446  fsuppind  42563  prjsprellsp  42584  lzenom  42743  rmxycomplete  42890  fzneg  42955  modabsdifz  42959  jm2.19  42966  pw2f1ocnv  43010  nadd1suc  43365  fzunt  43428  fzuntd  43429  fzunt1d  43430  fzuntgd  43431  sqrtcvallem1  43604  brtrclfv2  43700  rfovcnvf1od  43977  ntrclsfveq1  44033  ntrclsiso  44040  k0004lem2  44121  caofcan  44296  rfcnpre1  44997  rfcnpre2  45009  ellimcabssub0  45599  liminfpnfuz  45798  xlimpnfxnegmnf2  45840  fperdvper  45901  vonvolmbl  46643  readdcnnred  47288  resubcnnred  47289  cndivrenred  47291  submodaddmod  47326  minusmodnep2tmod  47338  requad2  47608  uhgrimisgrgric  47916  clnbgrgrim  47919  lco0  48413  lindslininds  48450  ltsubaddb  48500  ltsubsubb  48501  ltsubadd2b  48502  elbigolo1  48543  dig2bits  48600  rrx2pnedifcoorneorr  48703  mofeu  48833  sepnsepo  48909  lubeldm2d  48943  glbeldm2d  48944  cicpropdlem  49035  uptra  49201  uptr2a  49208  thincsect2  49454  thinccic  49457  isinito2lem  49484  postcposALT  49554  lanup  49627  ranup  49628  lmddu  49653