Theorem 3bitr4d 314

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  sbccomlem  3821  pr1eqbg  4815  unisucg  6464  fimarab  6985  fvopab3g  7014  fvimacnvALT  7082  respreima  7092  fmptco  7157  fnnfpeq0  7209  cocan1  7325  cocan2  7326  caofidlcan  7758  ordsucelsuc  7860  ordsucsssuc  7861  fnsuppres  8239  smoword  8405  oaword  8588  omword  8609  om00el  8615  oeword  8630  nnaword  8667  nnmword  8673  eldifsucnn  8704  naddss1  8730  naddunif  8734  swoer  8780  erth  8803  brecop  8862  eceqoveq  8874  xpdom2  9122  pw2f1olem  9131  ixpfi2  9370  cantnfrescl  9707  ttrclselem2  9757  rankr1bg  9841  r1pwcl  9891  fseqenlem1  10133  alephord3  10187  alephdom2  10196  engch  10743  fpwwe2lem6  10751  fpwwe2lem8  10753  ltexpi  11017  ltapi  11018  ltmpi  11019  ltsonq  11084  ltmnq  11087  1idpr  11144  addcanpr  11161  axpre-ltadd  11282  axlttri  11411  subsub23  11592  leadd1  11814  ltsub1  11842  ltsub2  11843  leord1  11873  eqord1  11874  lemul1  12199  lediv1  12212  lt2mul2div  12225  lerec  12230  lediv2  12237  le2msq  12247  suprleub  12313  infregelb  12331  ofsubeq0  12347  ofsubge0  12349  indpi1  12364  avgle1  12616  avgle2  12617  cnref1o  13143  xleneg  13378  xnn0lem1lt  13404  xltadd1  13416  xsubge0  13421  xposdif  13422  xltmul1  13452  supxrleub  13486  infxrgelb  13496  iooneg  13632  iccneg  13633  iccsplit  13646  iccshftr  13647  iccshftl  13649  iccdil  13651  icccntr  13653  fzsplit2  13713  fzaddel  13722  fzrev  13751  predfz  13817  elfzo  13825  nelfzo  13829  fzon  13845  elfzom1b  13931  negmod0  14048  leexp2  14344  ltexp2r  14346  repswsymball  14961  repswsymballbi  14962  cjreb  15322  sqrtlt  15460  limsuplt  15678  o1lo1  15736  rlimresb  15764  lo1eq  15767  rlimeq  15768  o1eq  15769  isercoll  15867  efle  16318  tanaddlem  16366  nndivdvds  16463  moddvds  16465  modmulconst  16490  oddm1even  16545  ltoddhalfle  16563  bitsp1  16633  sadcaddlem  16659  sadadd  16669  sadass  16673  bitsshft  16677  smuval2  16684  smumul  16695  dvdssq  16774  phiprmpw  16985  eulerthlem2  16991  odzdvds  17005  pc2dvds  17089  1arith  17137  imasleval  17745  mreacs  17864  catpropd  17915  oppcsect  17985  funcres2b  18104  fthsect  18134  fthinv  18135  fucsect  18182  fucinv  18183  latnlemlt  18678  latnle  18679  ipole  18740  ipolt  18741  mgmpropd  18861  issubg3  19387  eqgid  19424  qusxpid  19427  resghm2b  19480  conjghm  19495  ghmqusker  19534  gastacos  19557  resscntz  19580  cntzrec  19583  oppgsubm  19609  oppgsubg  19610  sylow3lem6  19879  lsmcom2  19902  lsmass  19916  ablsubsub23  20071  lsmcomx  20103  subgdmdprd  20283  opprsubrng  20844  opprsubrg  20878  lsslss  21269  lbspropd  21407  islbs2  21465  rspsn  21690  prmirred  21813  znfld  21899  lindfmm  22166  lindsmm  22167  lsslindf  22169  lsslinds  22170  islindf4  22177  psrbagconf1o  22270  gsumbagdiaglem  22272  mplmonmul  22378  basdif0  23304  neiptopreu  23484  neitr  23531  restlp  23534  cnrest2  23637  cnprest  23640  cnprest2  23641  lmss  23649  lmff  23652  ist1-2  23698  lpcls  23715  perfcls  23716  cmpfi  23759  hauseqlcld  23998  txlm  24000  txkgen  24004  xkopt  24007  idqtop  24058  tgqtop  24064  qtopcn  24066  uffix  24273  fmco  24313  flimrest  24335  lmflf  24357  txflf  24358  fclsrest  24376  cnpfcf  24393  tsmsgsum  24491  tsmsres  24496  tsmsf1o  24497  fmucndlem  24642  ismet2  24685  imasf1oxmet  24727  blres  24783  xmetec  24786  imasf1obl  24840  imasf1oxms  24841  prdsbl  24843  stdbdbl  24869  metrest  24876  metustsym  24907  blval2  24914  metuel2  24917  tngngp  25006  cnbl0  25125  cnblcld  25126  bl2ioo  25144  cncfcnvcn  25279  iihalf2  25287  icoopnst  25293  iocopnst  25294  icopnfcnv  25296  icopnfhmeo  25297  cphorthcom  25555  caucfil  25637  lmclim  25657  cmsss  25705  rrxmet  25762  volsup  25910  dyaddisjlem  25949  mbfeqalem1  25995  mbfeqalem2  25996  mbfeqa  25997  mbfmulc2lem  26001  mbfmax  26003  mbfposr  26006  ismbf3d  26008  mbfimaopnlem  26009  mbfaddlem  26014  mbfsup  26018  mbfinf  26019  0plef  26026  0pledm  26027  i1fmulclem  26056  i1fres  26059  i1fpos  26060  itg1climres  26068  mbfi1fseqlem4  26072  itg2mulclem  26100  itg2monolem1  26104  itg2cnlem1  26115  iblre  26147  iblcn  26152  itgeqa  26167  ellimc2  26230  limcflf  26234  dvreslem  26262  lhop1  26367  r1pid2  26513  ply1remlem  26516  fta1glem2  26520  ofmulrt  26633  plydiveu  26652  plyremlem  26658  rnplynfin  26663  quotcan  26665  ulmres  26748  cos11  26894  logleb  26964  argrege0  26972  logdivle  26983  efopn  27019  logccv  27024  cxplt  27055  cxple  27056  cxple2  27058  cxplt2  27059  cxplt3  27061  cxple3  27062  recxpf1lem  27090  logbleb  27144  logblt  27145  angrtmuld  27169  quad2  27200  atans2  27292  rlimcnp  27326  rlimcnp2  27327  rlimcxp  27334  sqff1o  27542  fsumvma2  27574  dchrptlem2  27625  lgsdilem  27684  lgsne0  27695  lgsqr  27711  lgsquadlem1  27740  lgsquadlem2  27741  m1lgs  27748  2lgslem1a  27751  2lgs  27767  dchrisum0lem1  27876  padicabv  27990  nosupinfsep  28122  oldlim  28306  newbday  28321  leslss  28328  ltadds2  28410  lenegs  28465  ltsubs2  28496  ltsubsubsbd  28502  lesubsubsbd  28505  lesubsubs2bd  28506  lesubsubs3bd  28507  lesubsd  28515  lemuls2d  28593  lemuls1d  28594  ltmulnegs1d  28595  onles  28687  n0subs2  28783  bdaypw2bnd  28884  bdayfinbndlem1  28886  trgcgrg  29011  colcom  29054  colrot1  29055  ishlg  29101  hlcomb  29102  hlbtwn  29110  lncom  29123  lnrot2  29125  israg  29205  perpcom  29221  hpgcom  29278  colopp  29280  plngcplem  29296  iscgra  29349  isinag  29390  dfprlng3  29459  colinearalglem2  29518  axcgrid  29527  uvtx01vtx  30011  iscplgredg  30031  rgrusgrprc  30203  uspgr2wlkeq  30259  dfpth2  30347  clwlkclwwlk  30626  eupth2lem3lem6  30867  fusgr2wsp2nb  30968  nmorepnf  31403  blocnilem  31439  ubthlem1  31505  shscom  31954  pjpreeq  32033  spansncol  32203  cmcm2  32251  hodsi  32410  nmoprepnf  32502  nmfnrepnf  32515  pjssposi  32807  cvcon3  32919  mdsymlem8  33045  dmdsym  33048  disjunsn  33263  unipreima  33312  fmptcof2  33326  fdifsupp  33352  ressupprn  33357  1stpreima  33374  fpwrelmapffslem  33397  infxrge0gelb  33431  nndiffz1  33451  prodindf  33502  indf1ofs  33506  mgccnv  33636  pwrssmgc  33637  gsumwrd2dccatlem  33714  cntzun  33716  cntrval2  33808  isinftm  33818  domnprodeq0  33916  lindfpropd  34021  lindspropd  34022  unitprodclb  34028  lsmssass  34037  nsgmgc  34047  crngmxidl  34078  opprqusdrng  34101  qsfld  34106  ply1dg1rt  34195  selvply1rhmlemb  34234  psrmonmul  34265  finexttrb  34380  algextdeglem7  34438  ist0cld  34548  metidv  34607  metider  34609  pstmxmet  34612  xrge0iifiso  34650  aean  34960  brfae  34964  signsply0  35263  signsvfn  35294  reprinrn  35330  subfacp1lem3  36127  subfacp1lem5  36129  fmlafvel  36330  opelco3  36730  sscoid  36866  cgrcomr  36953  ofscom  36963  cgr3permute3  37003  cgr3permute1  37004  cgr3com  37009  colinearperm1  37018  colinearperm3  37019  outsideofcom  37084  naddle  37159  opnbnd  37304  filnetlem4  37360  finxpsuclem  38525  wl-equsald  38676  wl-equsaldv  38677  lindsadd  38741  poimirlem23  38766  broucube  38777  heicant  38778  itg2addnclem2  38795  ftc1anclem1  38816  ftc1anclem5  38820  ftc1anclem6  38821  areacirclem5  38835  areacirc  38836  caures  38897  cnpwstotbnd  38934  ismtyima  38940  rrnmet  38966  reheibor  38976  rngosn3  39061  ecxrn2  39543  brcosscnvcoss  39659  br1cosscnvxrn  39699  eqvrelth  39830  brpartspart  40011  lcvbr  40281  lkrsc  40357  lshpkrlem1  40370  opltcon3b  40464  cmt2N  40510  cmt3N  40511  cvrcon3b  40537  cvrcmp2  40544  cvlexchb2  40591  cvlatexchb2  40595  2llnmj  40820  4atlem3  40856  4atlem9  40863  4atlem10a  40864  4atlem11a  40867  4atlem12a  40870  4at2  40874  2lplnmj  40882  llnexchb2  41129  lautlt  41351  lautcvr  41352  lautco  41357  ltrnatb  41397  ltrneq2  41408  cdlemefrs29pre00  41655  cdlemefrs29cpre1  41658  cdleme32fva  41697  dibglbN  42426  dochsncom  42642  dochkrsat  42715  lspindp5  43030  mapdh8ab  43037  hdmapip0com  43177  quadfac  43458  dvdsexpb  43591  sn-ltmul2d  43741  fsuppind  43822  prjsprellsp  43843  lzenom  43985  rmxycomplete  44128  fzneg  44193  modabsdifz  44197  jm2.19  44204  pw2f1ocnv  44248  nadd1suc  44597  fzunt  44659  fzuntd  44660  fzunt1d  44661  fzuntgd  44662  sqrtcvallem1  44834  brtrclfv2  44930  rfovcnvf1od  45207  ntrclsfveq1  45263  ntrclsiso  45270  k0004lem2  45351  caofcan  45510  cocanss1  46127  rfcnpre1  46252  rfcnpre2  46264  ellimcabssub0  46844  liminfpnfuz  47041  xlimpnfxnegmnf2  47083  fperdvper  47144  vonvolmbl  47886  tmachlem-agreeprod  48162  readdcnnred  48588  resubcnnred  48589  cndivrenred  48591  submodaddmod  48632  minusmodnep2tmod  48644  requad2  48936  uhgrimisgrgric  49244  clnbgrgrim  49247  lco0  49754  lindslininds  49791  ltsubaddb  49841  ltsubsubb  49842  ltsubadd2b  49843  elbigolo1  49884  dig2bits  49941  prelrrx2bd  50041  rrx2pnedifcoorneorr  50045  mofeu  50174  sepnsepo  50253  lubeldm2d  50287  glbeldm2d  50288  cicpropdlem  50378  uptra  50546  uptr2a  50553  thincsect2  50818  thinccic  50821  isinito2lem  50848  postcposALT  50921  lanup  51039  ranup  51040  lmddu  51065