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 205

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 206

This theorem is referenced by:  pr1eqbg  4857  unisucg  6440  fvopab3g  6991  fvimacnvALT  7056  respreima  7065  fmptco  7124  fnnfpeq0  7173  cocan1  7286  cocan2  7287  ordsucelsuc  7807  ordsucsssuc  7808  fnsuppres  8173  smoword  8363  oaword  8546  omword  8567  om00el  8573  oeword  8587  nnaword  8624  nnmword  8630  eldifsucnn  8660  naddss1  8685  naddunif  8689  swoer  8730  erth  8749  brecop  8801  eceqoveq  8813  xpdom2  9064  pw2f1olem  9073  ixpfi2  9347  cantnfrescl  9668  ttrclselem2  9718  rankr1bg  9795  r1pwcl  9839  fseqenlem1  10016  alephord3  10070  alephdom2  10079  engch  10620  fpwwe2lem6  10628  fpwwe2lem8  10630  ltexpi  10894  ltapi  10895  ltmpi  10896  ltsonq  10961  ltmnq  10964  1idpr  11021  addcanpr  11038  axpre-ltadd  11159  axlttri  11282  subsub23  11462  leadd1  11679  ltsub1  11707  ltsub2  11708  leord1  11738  eqord1  11739  lemul1  12063  lediv1  12076  lt2mul2div  12089  lerec  12094  lediv2  12101  le2msq  12111  suprleub  12177  infregelb  12195  ofsubeq0  12206  ofsubge0  12208  avgle1  12449  avgle2  12450  cnref1o  12966  xleneg  13194  xnn0lem1lt  13220  xltadd1  13232  xsubge0  13237  xposdif  13238  xltmul1  13268  supxrleub  13302  infxrgelb  13311  iooneg  13445  iccneg  13446  iccsplit  13459  iccshftr  13460  iccshftl  13462  iccdil  13464  icccntr  13466  fzsplit2  13523  fzaddel  13532  fzrev  13561  predfz  13623  elfzo  13631  nelfzo  13634  fzon  13650  elfzom1b  13728  negmod0  13840  leexp2  14133  ltexp2r  14135  repswsymball  14726  repswsymballbi  14727  cjreb  15067  sqrtlt  15205  limsuplt  15420  o1lo1  15478  rlimresb  15506  lo1eq  15509  rlimeq  15510  o1eq  15511  isercoll  15611  efle  16058  tanaddlem  16106  nndivdvds  16203  moddvds  16205  modmulconst  16228  oddm1even  16283  ltoddhalfle  16301  bitsp1  16369  sadcaddlem  16395  sadadd  16405  sadass  16409  bitsshft  16413  smuval2  16420  smumul  16431  dvdssq  16501  phiprmpw  16706  eulerthlem2  16712  odzdvds  16725  pc2dvds  16809  1arith  16857  imasleval  17484  mreacs  17599  catpropd  17650  oppcsect  17722  funcres2b  17844  fthsect  17873  fthinv  17874  fucsect  17922  fucinv  17923  latnlemlt  18422  latnle  18423  ipole  18484  ipolt  18485  issubg3  19019  eqgid  19055  resghm2b  19105  conjghm  19118  gastacos  19169  resscntz  19192  cntzrec  19195  oppgsubm  19224  oppgsubg  19225  sylow3lem6  19495  lsmcom2  19518  lsmass  19532  ablsubsub23  19687  lsmcomx  19719  subgdmdprd  19899  opprsubrg  20377  lsslss  20565  lbspropd  20703  islbs2  20760  rspsn  20885  prmirred  21036  znfld  21108  lindfmm  21374  lindsmm  21375  lsslindf  21377  lsslinds  21378  islindf4  21385  psrbagconf1o  21481  psrbagconf1oOLD  21482  gsumbagdiaglemOLD  21483  gsumbagdiaglem  21486  mplmonmul  21583  basdif0  22448  neiptopreu  22629  neitr  22676  restlp  22679  cnrest2  22782  cnprest  22785  cnprest2  22786  lmss  22794  lmff  22797  ist1-2  22843  lpcls  22860  perfcls  22861  cmpfi  22904  hauseqlcld  23142  txlm  23144  txkgen  23148  xkopt  23151  idqtop  23202  tgqtop  23208  qtopcn  23210  uffix  23417  fmco  23457  flimrest  23479  lmflf  23501  txflf  23502  fclsrest  23520  cnpfcf  23537  tsmsgsum  23635  tsmsres  23640  tsmsf1o  23641  fmucndlem  23788  ismet2  23831  imasf1oxmet  23873  blres  23929  xmetec  23932  imasf1obl  23989  imasf1oxms  23990  prdsbl  23992  stdbdbl  24018  metrest  24025  metustsym  24056  blval2  24063  metuel2  24066  tngngp  24163  cnbl0  24282  cnblcld  24283  bl2ioo  24300  cncfcnvcn  24433  iihalf2  24441  icoopnst  24447  iocopnst  24448  icopnfcnv  24450  icopnfhmeo  24451  cphorthcom  24710  caucfil  24792  lmclim  24812  cmsss  24860  rrxmet  24917  volsup  25065  dyaddisjlem  25104  mbfeqalem1  25150  mbfeqalem2  25151  mbfeqa  25152  mbfmulc2lem  25156  mbfmax  25158  mbfposr  25161  ismbf3d  25163  mbfimaopnlem  25164  mbfaddlem  25169  mbfsup  25173  mbfinf  25174  0plef  25181  0pledm  25182  i1fmulclem  25212  i1fres  25215  i1fpos  25216  itg1climres  25224  mbfi1fseqlem4  25228  itg2mulclem  25256  itg2monolem1  25260  itg2cnlem1  25271  iblre  25303  iblcn  25308  itgeqa  25323  ellimc2  25386  limcflf  25390  dvreslem  25418  lhop1  25523  ply1remlem  25672  fta1glem2  25676  ofmulrt  25787  plydiveu  25803  plyremlem  25809  quotcan  25814  ulmres  25892  cos11  26034  logleb  26103  argrege0  26111  logdivle  26122  efopn  26158  logccv  26163  cxplt  26194  cxple  26195  cxple2  26197  cxplt2  26198  cxplt3  26200  cxple3  26201  logbleb  26278  logblt  26279  angrtmuld  26303  quad2  26334  atans2  26426  rlimcnp  26460  rlimcnp2  26461  rlimcxp  26468  sqff1o  26676  fsumvma2  26707  dchrptlem2  26758  lgsdilem  26817  lgsne0  26828  lgsqr  26844  lgsquadlem1  26873  lgsquadlem2  26874  m1lgs  26881  2lgslem1a  26884  2lgs  26900  dchrisum0lem1  27009  padicabv  27123  nosupinfsep  27225  oldlim  27371  newbday  27386  sltadd2  27464  sleneg  27510  sltsub2  27534  sltsubsubbd  27540  slesubsubbd  27543  slesubsub2bd  27544  slesubsub3bd  27545  slemul2d  27616  slemul1d  27617  sltmulneg1d  27618  trgcgrg  27756  colcom  27799  colrot1  27800  ishlg  27843  hlcomb  27844  hlbtwn  27852  lncom  27863  lnrot2  27865  israg  27938  perpcom  27954  hpgcom  28008  colopp  28010  iscgra  28050  isinag  28079  colinearalglem2  28155  axcgrid  28164  uvtx01vtx  28644  iscplgredg  28664  rgrusgrprc  28836  uspgr2wlkeq  28893  clwlkclwwlk  29245  eupth2lem3lem6  29476  fusgr2wsp2nb  29577  nmorepnf  30009  blocnilem  30045  ubthlem1  30111  shscom  30560  pjpreeq  30639  spansncol  30809  cmcm2  30857  hodsi  31016  nmoprepnf  31108  nmfnrepnf  31121  pjssposi  31413  cvcon3  31525  mdsymlem8  31651  dmdsym  31654  disjunsn  31813  fimarab  31856  unipreima  31857  fmptcof2  31870  ressupprn  31900  1stpreima  31916  fpwrelmapffslem  31945  infxrge0gelb  31967  nndiffz1  31985  mgccnv  32157  pwrssmgc  32158  cntzun  32200  isinftm  32315  qusxpid  32464  lindfpropd  32487  lindspropd  32488  lsmssass  32501  nsgmgc  32512  ghmqusker  32521  crngmxidl  32574  opprqusdrng  32596  qsfld  32601  finexttrb  32730  ist0cld  32802  metidv  32861  metider  32863  pstmxmet  32866  xrge0iifiso  32904  indpi1  33007  prodindf  33010  indf1ofs  33013  aean  33231  brfae  33235  signsply0  33551  signsvfn  33582  reprinrn  33619  subfacp1lem3  34162  subfacp1lem5  34164  fmlafvel  34365  opelco3  34735  sscoid  34874  cgrcomr  34958  ofscom  34968  cgr3permute3  35008  cgr3permute1  35009  cgr3com  35014  colinearperm1  35023  colinearperm3  35024  outsideofcom  35089  opnbnd  35199  filnetlem4  35255  finxpsuclem  36267  wl-equsald  36397  lindsadd  36470  poimirlem23  36500  broucube  36511  heicant  36512  itg2addnclem2  36529  ftc1anclem1  36550  ftc1anclem5  36554  ftc1anclem6  36555  areacirclem5  36569  areacirc  36570  caures  36617  cnpwstotbnd  36654  ismtyima  36660  rrnmet  36686  reheibor  36696  rngosn3  36781  brcosscnvcoss  37293  br1cosscnvxrn  37333  eqvrelth  37470  brpartspart  37632  lcvbr  37880  lkrsc  37956  lshpkrlem1  37969  opltcon3b  38063  cmt2N  38109  cmt3N  38110  cvrcon3b  38136  cvrcmp2  38143  cvlexchb2  38190  cvlatexchb2  38194  2llnmj  38420  4atlem3  38456  4atlem9  38463  4atlem10a  38464  4atlem11a  38467  4atlem12a  38470  4at2  38474  2lplnmj  38482  llnexchb2  38729  lautlt  38951  lautcvr  38952  lautco  38957  ltrnatb  38997  ltrneq2  39008  cdlemefrs29pre00  39255  cdlemefrs29cpre1  39258  cdleme32fva  39297  dibglbN  40026  dochsncom  40242  dochkrsat  40315  lspindp5  40630  mapdh8ab  40637  hdmapip0com  40777  fsuppind  41160  dvdsexpb  41229  sn-ltmul2d  41331  prjsprellsp  41350  lzenom  41494  rmxycomplete  41642  fzneg  41707  modabsdifz  41711  jm2.19  41718  pw2f1ocnv  41762  nadd1suc  42128  fzunt  42192  fzuntd  42193  fzunt1d  42194  fzuntgd  42195  sqrtcvallem1  42368  brtrclfv2  42464  rfovcnvf1od  42741  ntrclsfveq1  42797  ntrclsiso  42804  k0004lem2  42885  caofcan  43068  rfcnpre1  43689  rfcnpre2  43701  ellimcabssub0  44320  liminfpnfuz  44519  xlimpnfxnegmnf2  44561  fperdvper  44622  vonvolmbl  45364  readdcnnred  45998  resubcnnred  45999  cndivrenred  46001  requad2  46278  mgmpropd  46532  opprsubrng  46723  lco0  47062  lindslininds  47099  ltsubaddb  47149  ltsubsubb  47150  ltsubadd2b  47151  elbigolo1  47197  dig2bits  47254  rrx2pnedifcoorneorr  47357  mofeu  47468  sepnsepo  47510  lubeldm2d  47545  glbeldm2d  47546  thincsect2  47632  thinccic  47635  postcposALT  47655