Theorem 3bitr4d 313

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

Syntax hints:   → wi 4   ↔ wb 208

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 209

This theorem is referenced by:  pr1eqbg  4787  fvopab3g  6763  fvimacnvALT  6827  respreima  6836  fmptco  6891  fnnfpeq0  6940  cocan1  7047  cocan2  7048  ordsucelsuc  7537  ordsucsssuc  7538  fnsuppres  7857  smoword  8003  oaword  8175  omword  8196  om00el  8202  oeword  8216  nnaword  8253  nnmword  8259  swoer  8319  erth  8338  brecop  8390  eceqoveq  8402  xpdom2  8612  pw2f1olem  8621  ixpfi2  8822  cantnfrescl  9139  rankr1bg  9232  r1pwcl  9276  fseqenlem1  9450  alephord3  9504  alephdom2  9513  engch  10050  fpwwe2lem7  10058  fpwwe2lem9  10060  ltexpi  10324  ltapi  10325  ltmpi  10326  ltsonq  10391  ltmnq  10394  1idpr  10451  addcanpr  10468  axpre-ltadd  10589  axlttri  10712  subsub23  10891  leadd1  11108  ltsub1  11136  ltsub2  11137  leord1  11167  eqord1  11168  lemul1  11492  lediv1  11505  lt2mul2div  11518  lerec  11523  lediv2  11530  le2msq  11540  suprleub  11607  infregelb  11625  ofsubeq0  11635  ofsubge0  11637  avgle1  11878  avgle2  11879  cnref1o  12385  xleneg  12612  xnn0lem1lt  12638  xltadd1  12650  xsubge0  12655  xposdif  12656  xltmul1  12686  supxrleub  12720  infxrgelb  12729  iooneg  12858  iccneg  12859  iccsplit  12872  iccshftr  12873  iccshftl  12875  iccdil  12877  icccntr  12879  fzsplit2  12933  fzaddel  12942  fzrev  12971  predfz  13033  elfzo  13041  nelfzo  13044  fzon  13059  elfzom1b  13137  negmod0  13247  leexp2  13536  ltexp2r  13538  repswsymball  14141  repswsymballbi  14142  cjreb  14482  sqrtlt  14621  limsuplt  14836  o1lo1  14894  rlimresb  14922  lo1eq  14925  rlimeq  14926  o1eq  14927  isercoll  15024  efle  15471  tanaddlem  15519  nndivdvds  15616  moddvds  15618  modmulconst  15641  oddm1even  15692  ltoddhalfle  15710  bitsp1  15780  sadcaddlem  15806  sadadd  15816  sadass  15820  bitsshft  15824  smuval2  15831  smumul  15842  dvdssq  15911  phiprmpw  16113  eulerthlem2  16119  odzdvds  16132  pc2dvds  16215  1arith  16263  imasleval  16814  mreacs  16929  catpropd  16979  oppcsect  17048  funcres2b  17167  fthsect  17195  fthinv  17196  fucsect  17242  fucinv  17243  latnlemlt  17694  latnle  17695  ipole  17768  ipolt  17769  issubg3  18297  eqgid  18332  resghm2b  18376  conjghm  18389  gastacos  18440  resscntz  18462  cntzrec  18464  oppgsubm  18490  oppgsubg  18491  sylow3lem6  18757  lsmcom2  18780  lsmass  18795  ablsubsub23  18945  lsmcomx  18976  subgdmdprd  19156  opprsubrg  19556  lsslss  19733  lbspropd  19871  islbs2  19926  rspsn  20027  psrbagconf1o  20154  gsumbagdiaglem  20155  mplmonmul  20245  prmirred  20642  znfld  20707  lindfmm  20971  lindsmm  20972  lsslindf  20974  lsslinds  20975  islindf4  20982  basdif0  21561  neiptopreu  21741  neitr  21788  restlp  21791  cnrest2  21894  cnprest  21897  cnprest2  21898  lmss  21906  lmff  21909  ist1-2  21955  lpcls  21972  perfcls  21973  cmpfi  22016  hauseqlcld  22254  txlm  22256  txkgen  22260  xkopt  22263  idqtop  22314  tgqtop  22320  qtopcn  22322  uffix  22529  fmco  22569  flimrest  22591  lmflf  22613  txflf  22614  fclsrest  22632  cnpfcf  22649  tsmsgsum  22747  tsmsres  22752  tsmsf1o  22753  fmucndlem  22900  ismet2  22943  imasf1oxmet  22985  blres  23041  xmetec  23044  imasf1obl  23098  imasf1oxms  23099  prdsbl  23101  stdbdbl  23127  metrest  23134  metustsym  23165  blval2  23172  metuel2  23175  tngngp  23263  cnbl0  23382  cnblcld  23383  bl2ioo  23400  cncfcnvcn  23529  iihalf2  23537  icoopnst  23543  iocopnst  23544  icopnfcnv  23546  icopnfhmeo  23547  cphorthcom  23805  caucfil  23886  lmclim  23906  cmsss  23954  rrxmet  24011  volsup  24157  dyaddisjlem  24196  mbfeqalem1  24242  mbfeqalem2  24243  mbfeqa  24244  mbfmulc2lem  24248  mbfmax  24250  mbfposr  24253  ismbf3d  24255  mbfimaopnlem  24256  mbfaddlem  24261  mbfsup  24265  mbfinf  24266  0plef  24273  0pledm  24274  i1fmulclem  24303  i1fres  24306  i1fpos  24307  itg1climres  24315  mbfi1fseqlem4  24319  itg2mulclem  24347  itg2monolem1  24351  itg2cnlem1  24362  iblre  24394  iblcn  24399  itgeqa  24414  ellimc2  24475  limcflf  24479  dvreslem  24507  lhop1  24611  ply1remlem  24756  fta1glem2  24760  ofmulrt  24871  plydiveu  24887  plyremlem  24893  quotcan  24898  ulmres  24976  cos11  25117  logleb  25186  argrege0  25194  logdivle  25205  efopn  25241  logccv  25246  cxplt  25277  cxple  25278  cxple2  25280  cxplt2  25281  cxplt3  25283  cxple3  25284  logbleb  25361  logblt  25362  angrtmuld  25386  quad2  25417  atans2  25509  rlimcnp  25543  rlimcnp2  25544  rlimcxp  25551  sqff1o  25759  fsumvma2  25790  dchrptlem2  25841  lgsdilem  25900  lgsne0  25911  lgsqr  25927  lgsquadlem1  25956  lgsquadlem2  25957  m1lgs  25964  2lgslem1a  25967  2lgs  25983  dchrisum0lem1  26092  padicabv  26206  trgcgrg  26301  colcom  26344  colrot1  26345  ishlg  26388  hlcomb  26389  hlbtwn  26397  lncom  26408  lnrot2  26410  israg  26483  perpcom  26499  hpgcom  26553  colopp  26555  iscgra  26595  isinag  26624  colinearalglem2  26693  axcgrid  26702  uvtx01vtx  27179  iscplgredg  27199  rgrusgrprc  27371  uspgr2wlkeq  27427  clwlkclwwlk  27780  eupth2lem3lem6  28012  fusgr2wsp2nb  28113  nmorepnf  28545  blocnilem  28581  ubthlem1  28647  shscom  29096  pjpreeq  29175  spansncol  29345  cmcm2  29393  hodsi  29552  nmoprepnf  29644  nmfnrepnf  29657  pjssposi  29949  cvcon3  30061  mdsymlem8  30187  dmdsym  30190  disjunsn  30344  fimarab  30390  unipreima  30391  fmptcof2  30402  1stpreima  30442  fpwrelmapffslem  30468  infxrge0gelb  30490  nndiffz1  30509  cntzun  30695  isinftm  30810  qusxpid  30928  lindfpropd  30942  lindspropd  30943  finexttrb  31052  metidv  31132  metider  31134  pstmxmet  31137  xrge0iifiso  31178  indpi1  31279  prodindf  31282  indf1ofs  31285  aean  31503  brfae  31507  signsply0  31821  signsvfn  31852  reprinrn  31889  subfacp1lem3  32429  subfacp1lem5  32431  fmlafvel  32632  opelco3  33018  sscoid  33374  cgrcomr  33458  ofscom  33468  cgr3permute3  33508  cgr3permute1  33509  cgr3com  33514  colinearperm1  33523  colinearperm3  33524  outsideofcom  33589  opnbnd  33673  filnetlem4  33729  finxpsuclem  34681  wl-equsald  34794  lindsadd  34900  poimirlem23  34930  broucube  34941  heicant  34942  itg2addnclem2  34959  ftc1anclem1  34982  ftc1anclem5  34986  ftc1anclem6  34987  areacirclem5  35001  areacirc  35002  caures  35050  cnpwstotbnd  35090  ismtyima  35096  rrnmet  35122  reheibor  35132  rngosn3  35217  brcosscnvcoss  35694  br1cosscnvxrn  35729  eqvrelth  35861  lcvbr  36172  lkrsc  36248  lshpkrlem1  36261  opltcon3b  36355  cmt2N  36401  cmt3N  36402  cvrcon3b  36428  cvrcmp2  36435  cvlexchb2  36482  cvlatexchb2  36486  2llnmj  36711  4atlem3  36747  4atlem9  36754  4atlem10a  36755  4atlem11a  36758  4atlem12a  36761  4at2  36765  2lplnmj  36773  llnexchb2  37020  lautlt  37242  lautcvr  37243  lautco  37248  ltrnatb  37288  ltrneq2  37299  cdlemefrs29pre00  37546  cdlemefrs29cpre1  37549  cdleme32fva  37588  dibglbN  38317  dochsncom  38533  dochkrsat  38606  lspindp5  38921  mapdh8ab  38928  hdmapip0com  39068  prjsprellsp  39281  lzenom  39387  rmxycomplete  39534  fzneg  39599  modabsdifz  39603  jm2.19  39610  pw2f1ocnv  39654  brtrclfv2  40092  rfovcnvf1od  40370  ntrclsfveq1  40430  ntrclsiso  40437  k0004lem2  40518  caofcan  40675  rfcnpre1  41296  rfcnpre2  41308  ellimcabssub0  41918  liminfpnfuz  42117  xlimpnfxnegmnf2  42159  fperdvper  42223  vonvolmbl  42963  readdcnnred  43523  resubcnnred  43524  cndivrenred  43526  requad2  43808  mgmpropd  44062  lco0  44502  lindslininds  44539  ltsubaddb  44589  ltsubsubb  44590  ltsubadd2b  44591  elbigolo1  44637  dig2bits  44694  rrx2pnedifcoorneorr  44724