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  3891  pr1eqbg  4881  unisucg  6473  fimarab  6996  fvopab3g  7024  fvimacnvALT  7090  respreima  7099  fmptco  7163  fnnfpeq0  7212  cocan1  7327  cocan2  7328  ordsucelsuc  7858  ordsucsssuc  7859  fnsuppres  8232  smoword  8422  oaword  8605  omword  8626  om00el  8632  oeword  8646  nnaword  8683  nnmword  8689  eldifsucnn  8720  naddss1  8745  naddunif  8749  swoer  8794  erth  8814  brecop  8868  eceqoveq  8880  xpdom2  9133  pw2f1olem  9142  ixpfi2  9420  cantnfrescl  9745  ttrclselem2  9795  rankr1bg  9872  r1pwcl  9916  fseqenlem1  10093  alephord3  10147  alephdom2  10156  engch  10697  fpwwe2lem6  10705  fpwwe2lem8  10707  ltexpi  10971  ltapi  10972  ltmpi  10973  ltsonq  11038  ltmnq  11041  1idpr  11098  addcanpr  11115  axpre-ltadd  11236  axlttri  11361  subsub23  11541  leadd1  11758  ltsub1  11786  ltsub2  11787  leord1  11817  eqord1  11818  lemul1  12146  lediv1  12160  lt2mul2div  12173  lerec  12178  lediv2  12185  le2msq  12195  suprleub  12261  infregelb  12279  ofsubeq0  12290  ofsubge0  12292  avgle1  12533  avgle2  12534  cnref1o  13050  xleneg  13280  xnn0lem1lt  13306  xltadd1  13318  xsubge0  13323  xposdif  13324  xltmul1  13354  supxrleub  13388  infxrgelb  13397  iooneg  13531  iccneg  13532  iccsplit  13545  iccshftr  13546  iccshftl  13548  iccdil  13550  icccntr  13552  fzsplit2  13609  fzaddel  13618  fzrev  13647  predfz  13710  elfzo  13718  nelfzo  13721  fzon  13737  elfzom1b  13816  negmod0  13929  leexp2  14221  ltexp2r  14223  repswsymball  14827  repswsymballbi  14828  cjreb  15172  sqrtlt  15310  limsuplt  15525  o1lo1  15583  rlimresb  15611  lo1eq  15614  rlimeq  15615  o1eq  15616  isercoll  15716  efle  16166  tanaddlem  16214  nndivdvds  16311  moddvds  16313  modmulconst  16336  oddm1even  16391  ltoddhalfle  16409  bitsp1  16477  sadcaddlem  16503  sadadd  16513  sadass  16517  bitsshft  16521  smuval2  16528  smumul  16539  dvdssq  16614  phiprmpw  16823  eulerthlem2  16829  odzdvds  16842  pc2dvds  16926  1arith  16974  imasleval  17601  mreacs  17716  catpropd  17767  oppcsect  17839  funcres2b  17961  fthsect  17992  fthinv  17993  fucsect  18042  fucinv  18043  latnlemlt  18542  latnle  18543  ipole  18604  ipolt  18605  mgmpropd  18689  issubg3  19184  eqgid  19220  resghm2b  19274  conjghm  19289  ghmqusker  19327  gastacos  19350  resscntz  19373  cntzrec  19376  oppgsubm  19405  oppgsubg  19406  sylow3lem6  19674  lsmcom2  19697  lsmass  19711  ablsubsub23  19866  lsmcomx  19898  subgdmdprd  20078  opprsubrng  20585  opprsubrg  20621  lsslss  20982  lbspropd  21121  islbs2  21179  rspsn  21366  prmirred  21508  znfld  21602  lindfmm  21870  lindsmm  21871  lsslindf  21873  lsslinds  21874  islindf4  21881  psrbagconf1o  21972  gsumbagdiaglem  21973  mplmonmul  22077  basdif0  22981  neiptopreu  23162  neitr  23209  restlp  23212  cnrest2  23315  cnprest  23318  cnprest2  23319  lmss  23327  lmff  23330  ist1-2  23376  lpcls  23393  perfcls  23394  cmpfi  23437  hauseqlcld  23675  txlm  23677  txkgen  23681  xkopt  23684  idqtop  23735  tgqtop  23741  qtopcn  23743  uffix  23950  fmco  23990  flimrest  24012  lmflf  24034  txflf  24035  fclsrest  24053  cnpfcf  24070  tsmsgsum  24168  tsmsres  24173  tsmsf1o  24174  fmucndlem  24321  ismet2  24364  imasf1oxmet  24406  blres  24462  xmetec  24465  imasf1obl  24522  imasf1oxms  24523  prdsbl  24525  stdbdbl  24551  metrest  24558  metustsym  24589  blval2  24596  metuel2  24599  tngngp  24696  cnbl0  24815  cnblcld  24816  bl2ioo  24833  cncfcnvcn  24971  iihalf2  24980  icoopnst  24988  iocopnst  24989  icopnfcnv  24992  icopnfhmeo  24993  cphorthcom  25254  caucfil  25336  lmclim  25356  cmsss  25404  rrxmet  25461  volsup  25610  dyaddisjlem  25649  mbfeqalem1  25695  mbfeqalem2  25696  mbfeqa  25697  mbfmulc2lem  25701  mbfmax  25703  mbfposr  25706  ismbf3d  25708  mbfimaopnlem  25709  mbfaddlem  25714  mbfsup  25718  mbfinf  25719  0plef  25726  0pledm  25727  i1fmulclem  25757  i1fres  25760  i1fpos  25761  itg1climres  25769  mbfi1fseqlem4  25773  itg2mulclem  25801  itg2monolem1  25805  itg2cnlem1  25816  iblre  25849  iblcn  25854  itgeqa  25869  ellimc2  25932  limcflf  25936  dvreslem  25964  lhop1  26073  r1pid2  26221  ply1remlem  26224  fta1glem2  26228  ofmulrt  26341  plydiveu  26358  plyremlem  26364  quotcan  26369  ulmres  26449  cos11  26593  logleb  26663  argrege0  26671  logdivle  26682  efopn  26718  logccv  26723  cxplt  26754  cxple  26755  cxple2  26757  cxplt2  26758  cxplt3  26760  cxple3  26761  recxpf1lem  26789  logbleb  26844  logblt  26845  angrtmuld  26869  quad2  26900  atans2  26992  rlimcnp  27026  rlimcnp2  27027  rlimcxp  27035  sqff1o  27243  fsumvma2  27276  dchrptlem2  27327  lgsdilem  27386  lgsne0  27397  lgsqr  27413  lgsquadlem1  27442  lgsquadlem2  27443  m1lgs  27450  2lgslem1a  27453  2lgs  27469  dchrisum0lem1  27578  padicabv  27692  nosupinfsep  27795  oldlim  27943  newbday  27958  slelss  27964  sltadd2  28042  sleneg  28096  sltsub2  28125  sltsubsubbd  28131  slesubsubbd  28134  slesubsub2bd  28135  slesubsub3bd  28136  slemul2d  28218  slemul1d  28219  sltmulneg1d  28220  trgcgrg  28541  colcom  28584  colrot1  28585  ishlg  28628  hlcomb  28629  hlbtwn  28637  lncom  28648  lnrot2  28650  israg  28723  perpcom  28739  hpgcom  28793  colopp  28795  iscgra  28835  isinag  28864  colinearalglem2  28940  axcgrid  28949  uvtx01vtx  29432  iscplgredg  29452  rgrusgrprc  29625  uspgr2wlkeq  29682  clwlkclwwlk  30034  eupth2lem3lem6  30265  fusgr2wsp2nb  30366  nmorepnf  30800  blocnilem  30836  ubthlem1  30902  shscom  31351  pjpreeq  31430  spansncol  31600  cmcm2  31648  hodsi  31807  nmoprepnf  31899  nmfnrepnf  31912  pjssposi  32204  cvcon3  32316  mdsymlem8  32442  dmdsym  32445  disjunsn  32616  unipreima  32662  fmptcof2  32675  ressupprn  32702  1stpreima  32718  fpwrelmapffslem  32746  infxrge0gelb  32773  nndiffz1  32791  mgccnv  32972  pwrssmgc  32973  cntzun  33044  isinftm  33161  qusxpid  33356  lindfpropd  33375  lindspropd  33376  unitprodclb  33382  lsmssass  33395  nsgmgc  33405  crngmxidl  33462  opprqusdrng  33486  qsfld  33491  ply1dg1rt  33569  finexttrb  33675  algextdeglem7  33714  ist0cld  33779  metidv  33838  metider  33840  pstmxmet  33843  xrge0iifiso  33881  indpi1  33984  prodindf  33987  indf1ofs  33990  aean  34208  brfae  34212  signsply0  34528  signsvfn  34559  reprinrn  34595  subfacp1lem3  35150  subfacp1lem5  35152  fmlafvel  35353  opelco3  35738  sscoid  35877  cgrcomr  35961  ofscom  35971  cgr3permute3  36011  cgr3permute1  36012  cgr3com  36017  colinearperm1  36026  colinearperm3  36027  outsideofcom  36092  opnbnd  36291  filnetlem4  36347  finxpsuclem  37363  wl-equsald  37493  wl-equsaldv  37494  lindsadd  37573  poimirlem23  37603  broucube  37614  heicant  37615  itg2addnclem2  37632  ftc1anclem1  37653  ftc1anclem5  37657  ftc1anclem6  37658  areacirclem5  37672  areacirc  37673  caures  37720  cnpwstotbnd  37757  ismtyima  37763  rrnmet  37789  reheibor  37799  rngosn3  37884  brcosscnvcoss  38390  br1cosscnvxrn  38430  eqvrelth  38567  brpartspart  38729  lcvbr  38977  lkrsc  39053  lshpkrlem1  39066  opltcon3b  39160  cmt2N  39206  cmt3N  39207  cvrcon3b  39233  cvrcmp2  39240  cvlexchb2  39287  cvlatexchb2  39291  2llnmj  39517  4atlem3  39553  4atlem9  39560  4atlem10a  39561  4atlem11a  39564  4atlem12a  39567  4at2  39571  2lplnmj  39579  llnexchb2  39826  lautlt  40048  lautcvr  40049  lautco  40054  ltrnatb  40094  ltrneq2  40105  cdlemefrs29pre00  40352  cdlemefrs29cpre1  40355  cdleme32fva  40394  dibglbN  41123  dochsncom  41339  dochkrsat  41412  lspindp5  41727  mapdh8ab  41734  hdmapip0com  41874  dvdsexpb  42322  sn-ltmul2d  42437  fsuppind  42545  prjsprellsp  42566  lzenom  42726  rmxycomplete  42874  fzneg  42939  modabsdifz  42943  jm2.19  42950  pw2f1ocnv  42994  nadd1suc  43354  fzunt  43417  fzuntd  43418  fzunt1d  43419  fzuntgd  43420  sqrtcvallem1  43593  brtrclfv2  43689  rfovcnvf1od  43966  ntrclsfveq1  44022  ntrclsiso  44029  k0004lem2  44110  caofcan  44292  rfcnpre1  44919  rfcnpre2  44931  ellimcabssub0  45538  liminfpnfuz  45737  xlimpnfxnegmnf2  45779  fperdvper  45840  vonvolmbl  46582  readdcnnred  47218  resubcnnred  47219  cndivrenred  47221  requad2  47497  uhgrimisgrgric  47783  clnbgrgrim  47786  lco0  48156  lindslininds  48193  ltsubaddb  48243  ltsubsubb  48244  ltsubadd2b  48245  elbigolo1  48291  dig2bits  48348  rrx2pnedifcoorneorr  48451  mofeu  48561  sepnsepo  48603  lubeldm2d  48638  glbeldm2d  48639  thincsect2  48725  thinccic  48728  postcposALT  48748