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  3821  pr1eqbg  4808  unisucg  6387  fimarab  6897  fvopab3g  6925  fvimacnvALT  6991  respreima  7000  fmptco  7063  fnnfpeq0  7114  cocan1  7228  cocan2  7229  caofidlcan  7651  ordsucelsuc  7755  ordsucsssuc  7756  fnsuppres  8124  smoword  8289  oaword  8467  omword  8488  om00el  8494  oeword  8508  nnaword  8545  nnmword  8551  eldifsucnn  8582  naddss1  8607  naddunif  8611  swoer  8656  erth  8679  brecop  8737  eceqoveq  8749  xpdom2  8989  pw2f1olem  8998  ixpfi2  9240  cantnfrescl  9572  ttrclselem2  9622  rankr1bg  9699  r1pwcl  9743  fseqenlem1  9918  alephord3  9972  alephdom2  9981  engch  10522  fpwwe2lem6  10530  fpwwe2lem8  10532  ltexpi  10796  ltapi  10797  ltmpi  10798  ltsonq  10863  ltmnq  10866  1idpr  10923  addcanpr  10940  axpre-ltadd  11061  axlttri  11187  subsub23  11368  leadd1  11588  ltsub1  11616  ltsub2  11617  leord1  11647  eqord1  11648  lemul1  11976  lediv1  11990  lt2mul2div  12003  lerec  12008  lediv2  12015  le2msq  12025  suprleub  12091  infregelb  12109  ofsubeq0  12125  ofsubge0  12127  avgle1  12364  avgle2  12365  cnref1o  12886  xleneg  13120  xnn0lem1lt  13146  xltadd1  13158  xsubge0  13163  xposdif  13164  xltmul1  13194  supxrleub  13228  infxrgelb  13238  iooneg  13374  iccneg  13375  iccsplit  13388  iccshftr  13389  iccshftl  13391  iccdil  13393  icccntr  13395  fzsplit2  13452  fzaddel  13461  fzrev  13490  predfz  13556  elfzo  13564  nelfzo  13567  fzon  13583  elfzom1b  13669  negmod0  13782  leexp2  14078  ltexp2r  14080  repswsymball  14685  repswsymballbi  14686  cjreb  15030  sqrtlt  15168  limsuplt  15386  o1lo1  15444  rlimresb  15472  lo1eq  15475  rlimeq  15476  o1eq  15477  isercoll  15575  efle  16027  tanaddlem  16075  nndivdvds  16172  moddvds  16174  modmulconst  16199  oddm1even  16254  ltoddhalfle  16272  bitsp1  16342  sadcaddlem  16368  sadadd  16378  sadass  16382  bitsshft  16386  smuval2  16393  smumul  16404  dvdssq  16478  phiprmpw  16687  eulerthlem2  16693  odzdvds  16707  pc2dvds  16791  1arith  16839  imasleval  17445  mreacs  17564  catpropd  17615  oppcsect  17685  funcres2b  17804  fthsect  17834  fthinv  17835  fucsect  17882  fucinv  17883  latnlemlt  18378  latnle  18379  ipole  18440  ipolt  18441  mgmpropd  18525  issubg3  19023  eqgid  19059  resghm2b  19113  conjghm  19128  ghmqusker  19166  gastacos  19189  resscntz  19212  cntzrec  19215  oppgsubm  19241  oppgsubg  19242  sylow3lem6  19511  lsmcom2  19534  lsmass  19548  ablsubsub23  19703  lsmcomx  19735  subgdmdprd  19915  opprsubrng  20444  opprsubrg  20478  lsslss  20864  lbspropd  21003  islbs2  21061  rspsn  21240  prmirred  21381  znfld  21467  lindfmm  21734  lindsmm  21735  lsslindf  21737  lsslinds  21738  islindf4  21745  psrbagconf1o  21836  gsumbagdiaglem  21837  mplmonmul  21941  basdif0  22838  neiptopreu  23018  neitr  23065  restlp  23068  cnrest2  23171  cnprest  23174  cnprest2  23175  lmss  23183  lmff  23186  ist1-2  23232  lpcls  23249  perfcls  23250  cmpfi  23293  hauseqlcld  23531  txlm  23533  txkgen  23537  xkopt  23540  idqtop  23591  tgqtop  23597  qtopcn  23599  uffix  23806  fmco  23846  flimrest  23868  lmflf  23890  txflf  23891  fclsrest  23909  cnpfcf  23926  tsmsgsum  24024  tsmsres  24029  tsmsf1o  24030  fmucndlem  24176  ismet2  24219  imasf1oxmet  24261  blres  24317  xmetec  24320  imasf1obl  24374  imasf1oxms  24375  prdsbl  24377  stdbdbl  24403  metrest  24410  metustsym  24441  blval2  24448  metuel2  24451  tngngp  24540  cnbl0  24659  cnblcld  24660  bl2ioo  24678  cncfcnvcn  24817  iihalf2  24826  icoopnst  24834  iocopnst  24835  icopnfcnv  24838  icopnfhmeo  24839  cphorthcom  25099  caucfil  25181  lmclim  25201  cmsss  25249  rrxmet  25306  volsup  25455  dyaddisjlem  25494  mbfeqalem1  25540  mbfeqalem2  25541  mbfeqa  25542  mbfmulc2lem  25546  mbfmax  25548  mbfposr  25551  ismbf3d  25553  mbfimaopnlem  25554  mbfaddlem  25559  mbfsup  25563  mbfinf  25564  0plef  25571  0pledm  25572  i1fmulclem  25601  i1fres  25604  i1fpos  25605  itg1climres  25613  mbfi1fseqlem4  25617  itg2mulclem  25645  itg2monolem1  25649  itg2cnlem1  25660  iblre  25693  iblcn  25698  itgeqa  25713  ellimc2  25776  limcflf  25780  dvreslem  25808  lhop1  25917  r1pid2  26065  ply1remlem  26068  fta1glem2  26072  ofmulrt  26187  plydiveu  26204  plyremlem  26210  quotcan  26215  ulmres  26295  cos11  26440  logleb  26510  argrege0  26518  logdivle  26529  efopn  26565  logccv  26570  cxplt  26601  cxple  26602  cxple2  26604  cxplt2  26605  cxplt3  26607  cxple3  26608  recxpf1lem  26636  logbleb  26691  logblt  26692  angrtmuld  26716  quad2  26747  atans2  26839  rlimcnp  26873  rlimcnp2  26874  rlimcxp  26882  sqff1o  27090  fsumvma2  27123  dchrptlem2  27174  lgsdilem  27233  lgsne0  27244  lgsqr  27260  lgsquadlem1  27289  lgsquadlem2  27290  m1lgs  27297  2lgslem1a  27300  2lgs  27316  dchrisum0lem1  27425  padicabv  27539  nosupinfsep  27642  oldlim  27803  newbday  27818  slelss  27825  sltadd2  27905  sleneg  27959  sltsub2  27988  sltsubsubbd  27994  slesubsubbd  27997  slesubsub2bd  27998  slesubsub3bd  27999  slemul2d  28084  slemul1d  28085  sltmulneg1d  28086  n0subs2  28261  trgcgrg  28464  colcom  28507  colrot1  28508  ishlg  28551  hlcomb  28552  hlbtwn  28560  lncom  28571  lnrot2  28573  israg  28646  perpcom  28662  hpgcom  28716  colopp  28718  iscgra  28758  isinag  28787  colinearalglem2  28856  axcgrid  28865  uvtx01vtx  29346  iscplgredg  29366  rgrusgrprc  29539  uspgr2wlkeq  29595  dfpth2  29678  clwlkclwwlk  29950  eupth2lem3lem6  30181  fusgr2wsp2nb  30282  nmorepnf  30716  blocnilem  30752  ubthlem1  30818  shscom  31267  pjpreeq  31346  spansncol  31516  cmcm2  31564  hodsi  31723  nmoprepnf  31815  nmfnrepnf  31828  pjssposi  32120  cvcon3  32232  mdsymlem8  32358  dmdsym  32361  disjunsn  32543  unipreima  32594  fmptcof2  32608  fdifsupp  32635  ressupprn  32640  1stpreima  32657  fpwrelmapffslem  32684  infxrge0gelb  32718  nndiffz1  32738  indpi1  32812  prodindf  32815  indf1ofs  32818  mgccnv  32950  pwrssmgc  32951  gsumwrd2dccatlem  33028  cntzun  33030  cntrval2  33122  isinftm  33132  qusxpid  33309  lindfpropd  33328  lindspropd  33329  unitprodclb  33335  lsmssass  33348  nsgmgc  33358  crngmxidl  33415  opprqusdrng  33439  qsfld  33444  ply1dg1rt  33524  finexttrb  33648  algextdeglem7  33706  ist0cld  33816  metidv  33875  metider  33877  pstmxmet  33880  xrge0iifiso  33918  aean  34227  brfae  34231  signsply0  34535  signsvfn  34566  reprinrn  34602  subfacp1lem3  35175  subfacp1lem5  35177  fmlafvel  35378  opelco3  35768  sscoid  35907  cgrcomr  35991  ofscom  36001  cgr3permute3  36041  cgr3permute1  36042  cgr3com  36047  colinearperm1  36056  colinearperm3  36057  outsideofcom  36122  opnbnd  36319  filnetlem4  36375  finxpsuclem  37391  wl-equsald  37533  wl-equsaldv  37534  lindsadd  37613  poimirlem23  37643  broucube  37654  heicant  37655  itg2addnclem2  37672  ftc1anclem1  37693  ftc1anclem5  37697  ftc1anclem6  37698  areacirclem5  37712  areacirc  37713  caures  37760  cnpwstotbnd  37797  ismtyima  37803  rrnmet  37829  reheibor  37839  rngosn3  37924  brcosscnvcoss  38431  br1cosscnvxrn  38471  eqvrelth  38608  brpartspart  38771  lcvbr  39020  lkrsc  39096  lshpkrlem1  39109  opltcon3b  39203  cmt2N  39249  cmt3N  39250  cvrcon3b  39276  cvrcmp2  39283  cvlexchb2  39330  cvlatexchb2  39334  2llnmj  39559  4atlem3  39595  4atlem9  39602  4atlem10a  39603  4atlem11a  39606  4atlem12a  39609  4at2  39613  2lplnmj  39621  llnexchb2  39868  lautlt  40090  lautcvr  40091  lautco  40096  ltrnatb  40136  ltrneq2  40147  cdlemefrs29pre00  40394  cdlemefrs29cpre1  40397  cdleme32fva  40436  dibglbN  41165  dochsncom  41381  dochkrsat  41454  lspindp5  41769  mapdh8ab  41776  hdmapip0com  41916  dvdsexpb  42328  sn-ltmul2d  42466  fsuppind  42583  prjsprellsp  42604  lzenom  42763  rmxycomplete  42910  fzneg  42975  modabsdifz  42979  jm2.19  42986  pw2f1ocnv  43030  nadd1suc  43385  fzunt  43448  fzuntd  43449  fzunt1d  43450  fzuntgd  43451  sqrtcvallem1  43624  brtrclfv2  43720  rfovcnvf1od  43997  ntrclsfveq1  44053  ntrclsiso  44060  k0004lem2  44141  caofcan  44316  rfcnpre1  45017  rfcnpre2  45029  ellimcabssub0  45618  liminfpnfuz  45817  xlimpnfxnegmnf2  45859  fperdvper  45920  vonvolmbl  46662  readdcnnred  47307  resubcnnred  47308  cndivrenred  47310  submodaddmod  47345  minusmodnep2tmod  47357  requad2  47627  uhgrimisgrgric  47935  clnbgrgrim  47938  lco0  48432  lindslininds  48469  ltsubaddb  48519  ltsubsubb  48520  ltsubadd2b  48521  elbigolo1  48562  dig2bits  48619  rrx2pnedifcoorneorr  48722  mofeu  48852  sepnsepo  48928  lubeldm2d  48962  glbeldm2d  48963  cicpropdlem  49054  uptra  49220  uptr2a  49227  thincsect2  49473  thinccic  49476  isinito2lem  49503  postcposALT  49573  lanup  49646  ranup  49647  lmddu  49672