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  3869  pr1eqbg  4857  unisucg  6462  fimarab  6983  fvopab3g  7011  fvimacnvALT  7077  respreima  7086  fmptco  7149  fnnfpeq0  7198  cocan1  7311  cocan2  7312  caofidlcan  7735  ordsucelsuc  7842  ordsucsssuc  7843  fnsuppres  8216  smoword  8406  oaword  8587  omword  8608  om00el  8614  oeword  8628  nnaword  8665  nnmword  8671  eldifsucnn  8702  naddss1  8727  naddunif  8731  swoer  8776  erth  8796  brecop  8850  eceqoveq  8862  xpdom2  9107  pw2f1olem  9116  ixpfi2  9390  cantnfrescl  9716  ttrclselem2  9766  rankr1bg  9843  r1pwcl  9887  fseqenlem1  10064  alephord3  10118  alephdom2  10127  engch  10668  fpwwe2lem6  10676  fpwwe2lem8  10678  ltexpi  10942  ltapi  10943  ltmpi  10944  ltsonq  11009  ltmnq  11012  1idpr  11069  addcanpr  11086  axpre-ltadd  11207  axlttri  11332  subsub23  11513  leadd1  11731  ltsub1  11759  ltsub2  11760  leord1  11790  eqord1  11791  lemul1  12119  lediv1  12133  lt2mul2div  12146  lerec  12151  lediv2  12158  le2msq  12168  suprleub  12234  infregelb  12252  ofsubeq0  12263  ofsubge0  12265  avgle1  12506  avgle2  12507  cnref1o  13027  xleneg  13260  xnn0lem1lt  13286  xltadd1  13298  xsubge0  13303  xposdif  13304  xltmul1  13334  supxrleub  13368  infxrgelb  13377  iooneg  13511  iccneg  13512  iccsplit  13525  iccshftr  13526  iccshftl  13528  iccdil  13530  icccntr  13532  fzsplit2  13589  fzaddel  13598  fzrev  13627  predfz  13693  elfzo  13701  nelfzo  13704  fzon  13720  elfzom1b  13805  negmod0  13918  leexp2  14211  ltexp2r  14213  repswsymball  14817  repswsymballbi  14818  cjreb  15162  sqrtlt  15300  limsuplt  15515  o1lo1  15573  rlimresb  15601  lo1eq  15604  rlimeq  15605  o1eq  15606  isercoll  15704  efle  16154  tanaddlem  16202  nndivdvds  16299  moddvds  16301  modmulconst  16325  oddm1even  16380  ltoddhalfle  16398  bitsp1  16468  sadcaddlem  16494  sadadd  16504  sadass  16508  bitsshft  16512  smuval2  16519  smumul  16530  dvdssq  16604  phiprmpw  16813  eulerthlem2  16819  odzdvds  16833  pc2dvds  16917  1arith  16965  imasleval  17586  mreacs  17701  catpropd  17752  oppcsect  17822  funcres2b  17942  fthsect  17972  fthinv  17973  fucsect  18020  fucinv  18021  latnlemlt  18517  latnle  18518  ipole  18579  ipolt  18580  mgmpropd  18664  issubg3  19162  eqgid  19198  resghm2b  19252  conjghm  19267  ghmqusker  19305  gastacos  19328  resscntz  19351  cntzrec  19354  oppgsubm  19381  oppgsubg  19382  sylow3lem6  19650  lsmcom2  19673  lsmass  19687  ablsubsub23  19842  lsmcomx  19874  subgdmdprd  20054  opprsubrng  20559  opprsubrg  20593  lsslss  20959  lbspropd  21098  islbs2  21156  rspsn  21343  prmirred  21485  znfld  21579  lindfmm  21847  lindsmm  21848  lsslindf  21850  lsslinds  21851  islindf4  21858  psrbagconf1o  21949  gsumbagdiaglem  21950  mplmonmul  22054  basdif0  22960  neiptopreu  23141  neitr  23188  restlp  23191  cnrest2  23294  cnprest  23297  cnprest2  23298  lmss  23306  lmff  23309  ist1-2  23355  lpcls  23372  perfcls  23373  cmpfi  23416  hauseqlcld  23654  txlm  23656  txkgen  23660  xkopt  23663  idqtop  23714  tgqtop  23720  qtopcn  23722  uffix  23929  fmco  23969  flimrest  23991  lmflf  24013  txflf  24014  fclsrest  24032  cnpfcf  24049  tsmsgsum  24147  tsmsres  24152  tsmsf1o  24153  fmucndlem  24300  ismet2  24343  imasf1oxmet  24385  blres  24441  xmetec  24444  imasf1obl  24501  imasf1oxms  24502  prdsbl  24504  stdbdbl  24530  metrest  24537  metustsym  24568  blval2  24575  metuel2  24578  tngngp  24675  cnbl0  24794  cnblcld  24795  bl2ioo  24813  cncfcnvcn  24952  iihalf2  24961  icoopnst  24969  iocopnst  24970  icopnfcnv  24973  icopnfhmeo  24974  cphorthcom  25235  caucfil  25317  lmclim  25337  cmsss  25385  rrxmet  25442  volsup  25591  dyaddisjlem  25630  mbfeqalem1  25676  mbfeqalem2  25677  mbfeqa  25678  mbfmulc2lem  25682  mbfmax  25684  mbfposr  25687  ismbf3d  25689  mbfimaopnlem  25690  mbfaddlem  25695  mbfsup  25699  mbfinf  25700  0plef  25707  0pledm  25708  i1fmulclem  25737  i1fres  25740  i1fpos  25741  itg1climres  25749  mbfi1fseqlem4  25753  itg2mulclem  25781  itg2monolem1  25785  itg2cnlem1  25796  iblre  25829  iblcn  25834  itgeqa  25849  ellimc2  25912  limcflf  25916  dvreslem  25944  lhop1  26053  r1pid2  26201  ply1remlem  26204  fta1glem2  26208  ofmulrt  26323  plydiveu  26340  plyremlem  26346  quotcan  26351  ulmres  26431  cos11  26575  logleb  26645  argrege0  26653  logdivle  26664  efopn  26700  logccv  26705  cxplt  26736  cxple  26737  cxple2  26739  cxplt2  26740  cxplt3  26742  cxple3  26743  recxpf1lem  26771  logbleb  26826  logblt  26827  angrtmuld  26851  quad2  26882  atans2  26974  rlimcnp  27008  rlimcnp2  27009  rlimcxp  27017  sqff1o  27225  fsumvma2  27258  dchrptlem2  27309  lgsdilem  27368  lgsne0  27379  lgsqr  27395  lgsquadlem1  27424  lgsquadlem2  27425  m1lgs  27432  2lgslem1a  27435  2lgs  27451  dchrisum0lem1  27560  padicabv  27674  nosupinfsep  27777  oldlim  27925  newbday  27940  slelss  27946  sltadd2  28024  sleneg  28078  sltsub2  28107  sltsubsubbd  28113  slesubsubbd  28116  slesubsub2bd  28117  slesubsub3bd  28118  slemul2d  28200  slemul1d  28201  sltmulneg1d  28202  trgcgrg  28523  colcom  28566  colrot1  28567  ishlg  28610  hlcomb  28611  hlbtwn  28619  lncom  28630  lnrot2  28632  israg  28705  perpcom  28721  hpgcom  28775  colopp  28777  iscgra  28817  isinag  28846  colinearalglem2  28922  axcgrid  28931  uvtx01vtx  29414  iscplgredg  29434  rgrusgrprc  29607  uspgr2wlkeq  29664  dfpth2  29749  clwlkclwwlk  30021  eupth2lem3lem6  30252  fusgr2wsp2nb  30353  nmorepnf  30787  blocnilem  30823  ubthlem1  30889  shscom  31338  pjpreeq  31417  spansncol  31587  cmcm2  31635  hodsi  31794  nmoprepnf  31886  nmfnrepnf  31899  pjssposi  32191  cvcon3  32303  mdsymlem8  32429  dmdsym  32432  disjunsn  32607  unipreima  32653  fmptcof2  32667  fdifsupp  32694  ressupprn  32699  1stpreima  32716  fpwrelmapffslem  32743  infxrge0gelb  32770  nndiffz1  32788  indpi1  32845  prodindf  32848  indf1ofs  32851  mgccnv  32989  pwrssmgc  32990  gsumwrd2dccatlem  33069  cntzun  33071  isinftm  33188  qusxpid  33391  lindfpropd  33410  lindspropd  33411  unitprodclb  33417  lsmssass  33430  nsgmgc  33440  crngmxidl  33497  opprqusdrng  33521  qsfld  33526  ply1dg1rt  33604  finexttrb  33715  algextdeglem7  33764  ist0cld  33832  metidv  33891  metider  33893  pstmxmet  33896  xrge0iifiso  33934  aean  34245  brfae  34249  signsply0  34566  signsvfn  34597  reprinrn  34633  subfacp1lem3  35187  subfacp1lem5  35189  fmlafvel  35390  opelco3  35775  sscoid  35914  cgrcomr  35998  ofscom  36008  cgr3permute3  36048  cgr3permute1  36049  cgr3com  36054  colinearperm1  36063  colinearperm3  36064  outsideofcom  36129  opnbnd  36326  filnetlem4  36382  finxpsuclem  37398  wl-equsald  37540  wl-equsaldv  37541  lindsadd  37620  poimirlem23  37650  broucube  37661  heicant  37662  itg2addnclem2  37679  ftc1anclem1  37700  ftc1anclem5  37704  ftc1anclem6  37705  areacirclem5  37719  areacirc  37720  caures  37767  cnpwstotbnd  37804  ismtyima  37810  rrnmet  37836  reheibor  37846  rngosn3  37931  brcosscnvcoss  38435  br1cosscnvxrn  38475  eqvrelth  38612  brpartspart  38774  lcvbr  39022  lkrsc  39098  lshpkrlem1  39111  opltcon3b  39205  cmt2N  39251  cmt3N  39252  cvrcon3b  39278  cvrcmp2  39285  cvlexchb2  39332  cvlatexchb2  39336  2llnmj  39562  4atlem3  39598  4atlem9  39605  4atlem10a  39606  4atlem11a  39609  4atlem12a  39612  4at2  39616  2lplnmj  39624  llnexchb2  39871  lautlt  40093  lautcvr  40094  lautco  40099  ltrnatb  40139  ltrneq2  40150  cdlemefrs29pre00  40397  cdlemefrs29cpre1  40400  cdleme32fva  40439  dibglbN  41168  dochsncom  41384  dochkrsat  41457  lspindp5  41772  mapdh8ab  41779  hdmapip0com  41919  dvdsexpb  42370  sn-ltmul2d  42491  fsuppind  42600  prjsprellsp  42621  lzenom  42781  rmxycomplete  42929  fzneg  42994  modabsdifz  42998  jm2.19  43005  pw2f1ocnv  43049  nadd1suc  43405  fzunt  43468  fzuntd  43469  fzunt1d  43470  fzuntgd  43471  sqrtcvallem1  43644  brtrclfv2  43740  rfovcnvf1od  44017  ntrclsfveq1  44073  ntrclsiso  44080  k0004lem2  44161  caofcan  44342  rfcnpre1  45024  rfcnpre2  45036  ellimcabssub0  45632  liminfpnfuz  45831  xlimpnfxnegmnf2  45873  fperdvper  45934  vonvolmbl  46676  readdcnnred  47315  resubcnnred  47316  cndivrenred  47318  submodaddmod  47343  minusmodnep2tmod  47355  requad2  47610  uhgrimisgrgric  47899  clnbgrgrim  47902  lco0  48344  lindslininds  48381  ltsubaddb  48431  ltsubsubb  48432  ltsubadd2b  48433  elbigolo1  48478  dig2bits  48535  rrx2pnedifcoorneorr  48638  mofeu  48757  sepnsepo  48821  lubeldm2d  48855  glbeldm2d  48856  thincsect2  49115  thinccic  49118  postcposALT  49172