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  3816  pr1eqbg  4811  unisucg  6443  fimarab  6960  fvopab3g  6989  fvimacnvALT  7057  respreima  7066  fmptco  7131  fnnfpeq0  7184  cocan1  7300  cocan2  7301  caofidlcan  7732  ordsucelsuc  7834  ordsucsssuc  7835  fnsuppres  8212  smoword  8378  oaword  8561  omword  8582  om00el  8588  oeword  8603  nnaword  8640  nnmword  8646  eldifsucnn  8677  naddss1  8703  naddunif  8707  swoer  8753  erth  8776  brecop  8835  eceqoveq  8847  xpdom2  9095  pw2f1olem  9104  ixpfi2  9343  cantnfrescl  9681  ttrclselem2  9731  rankr1bg  9815  r1pwcl  9865  fseqenlem1  10107  alephord3  10161  alephdom2  10170  engch  10717  fpwwe2lem6  10725  fpwwe2lem8  10727  ltexpi  10991  ltapi  10992  ltmpi  10993  ltsonq  11058  ltmnq  11061  1idpr  11118  addcanpr  11135  axpre-ltadd  11256  axlttri  11385  subsub23  11566  leadd1  11788  ltsub1  11816  ltsub2  11817  leord1  11847  eqord1  11848  lemul1  12173  lediv1  12186  lt2mul2div  12199  lerec  12204  lediv2  12211  le2msq  12221  suprleub  12287  infregelb  12305  ofsubeq0  12321  ofsubge0  12323  indpi1  12338  avgle1  12590  avgle2  12591  cnref1o  13117  xleneg  13352  xnn0lem1lt  13378  xltadd1  13390  xsubge0  13395  xposdif  13396  xltmul1  13426  supxrleub  13460  infxrgelb  13470  iooneg  13606  iccneg  13607  iccsplit  13620  iccshftr  13621  iccshftl  13623  iccdil  13625  icccntr  13627  fzsplit2  13687  fzaddel  13696  fzrev  13725  predfz  13791  elfzo  13799  nelfzo  13803  fzon  13819  elfzom1b  13905  negmod0  14022  leexp2  14318  ltexp2r  14320  repswsymball  14935  repswsymballbi  14936  cjreb  15296  sqrtlt  15434  limsuplt  15652  o1lo1  15710  rlimresb  15738  lo1eq  15741  rlimeq  15742  o1eq  15743  isercoll  15841  efle  16292  tanaddlem  16340  nndivdvds  16437  moddvds  16439  modmulconst  16464  oddm1even  16519  ltoddhalfle  16537  bitsp1  16607  sadcaddlem  16633  sadadd  16643  sadass  16647  bitsshft  16651  smuval2  16658  smumul  16669  dvdssq  16748  phiprmpw  16959  eulerthlem2  16965  odzdvds  16979  pc2dvds  17063  1arith  17111  imasleval  17719  mreacs  17838  catpropd  17889  oppcsect  17959  funcres2b  18078  fthsect  18108  fthinv  18109  fucsect  18156  fucinv  18157  latnlemlt  18652  latnle  18653  ipole  18714  ipolt  18715  mgmpropd  18835  issubg3  19361  eqgid  19398  qusxpid  19401  resghm2b  19454  conjghm  19469  ghmqusker  19507  gastacos  19530  resscntz  19553  cntzrec  19556  oppgsubm  19582  oppgsubg  19583  sylow3lem6  19852  lsmcom2  19875  lsmass  19889  ablsubsub23  20044  lsmcomx  20076  subgdmdprd  20256  opprsubrng  20817  opprsubrg  20851  lsslss  21242  lbspropd  21380  islbs2  21438  rspsn  21663  prmirred  21786  znfld  21872  lindfmm  22139  lindsmm  22140  lsslindf  22142  lsslinds  22143  islindf4  22150  psrbagconf1o  22243  gsumbagdiaglem  22245  mplmonmul  22351  basdif0  23277  neiptopreu  23457  neitr  23504  restlp  23507  cnrest2  23610  cnprest  23613  cnprest2  23614  lmss  23622  lmff  23625  ist1-2  23671  lpcls  23688  perfcls  23689  cmpfi  23732  hauseqlcld  23971  txlm  23973  txkgen  23977  xkopt  23980  idqtop  24031  tgqtop  24037  qtopcn  24039  uffix  24246  fmco  24286  flimrest  24308  lmflf  24330  txflf  24331  fclsrest  24349  cnpfcf  24366  tsmsgsum  24464  tsmsres  24469  tsmsf1o  24470  fmucndlem  24615  ismet2  24658  imasf1oxmet  24700  blres  24756  xmetec  24759  imasf1obl  24813  imasf1oxms  24814  prdsbl  24816  stdbdbl  24842  metrest  24849  metustsym  24880  blval2  24887  metuel2  24890  tngngp  24979  cnbl0  25098  cnblcld  25099  bl2ioo  25117  cncfcnvcn  25252  iihalf2  25260  icoopnst  25266  iocopnst  25267  icopnfcnv  25269  icopnfhmeo  25270  cphorthcom  25528  caucfil  25610  lmclim  25630  cmsss  25678  rrxmet  25735  volsup  25883  dyaddisjlem  25922  mbfeqalem1  25968  mbfeqalem2  25969  mbfeqa  25970  mbfmulc2lem  25974  mbfmax  25976  mbfposr  25979  ismbf3d  25981  mbfimaopnlem  25982  mbfaddlem  25987  mbfsup  25991  mbfinf  25992  0plef  25999  0pledm  26000  i1fmulclem  26029  i1fres  26032  i1fpos  26033  itg1climres  26041  mbfi1fseqlem4  26045  itg2mulclem  26073  itg2monolem1  26077  itg2cnlem1  26088  iblre  26120  iblcn  26125  itgeqa  26140  ellimc2  26203  limcflf  26207  dvreslem  26235  lhop1  26340  r1pid2  26486  ply1remlem  26489  fta1glem2  26493  ofmulrt  26606  plydiveu  26625  plyremlem  26631  rnplynfin  26636  quotcan  26638  ulmres  26721  cos11  26867  logleb  26937  argrege0  26945  logdivle  26956  efopn  26992  logccv  26997  cxplt  27028  cxple  27029  cxple2  27031  cxplt2  27032  cxplt3  27034  cxple3  27035  recxpf1lem  27063  logbleb  27117  logblt  27118  angrtmuld  27142  quad2  27173  atans2  27265  rlimcnp  27299  rlimcnp2  27300  rlimcxp  27307  sqff1o  27515  fsumvma2  27547  dchrptlem2  27598  lgsdilem  27657  lgsne0  27668  lgsqr  27684  lgsquadlem1  27713  lgsquadlem2  27714  m1lgs  27721  2lgslem1a  27724  2lgs  27740  dchrisum0lem1  27849  padicabv  27963  nosupinfsep  28095  oldlim  28279  newbday  28294  leslss  28301  ltadds2  28383  lenegs  28438  ltsubs2  28469  ltsubsubsbd  28475  lesubsubsbd  28478  lesubsubs2bd  28479  lesubsubs3bd  28480  lesubsd  28488  lemuls2d  28566  lemuls1d  28567  ltmulnegs1d  28568  onles  28660  n0subs2  28756  bdaypw2bnd  28857  bdayfinbndlem1  28859  trgcgrg  28984  colcom  29027  colrot1  29028  ishlg  29074  hlcomb  29075  hlbtwn  29083  lncom  29096  lnrot2  29098  israg  29178  perpcom  29194  hpgcom  29251  colopp  29253  plngcplem  29269  iscgra  29322  isinag  29363  dfprlng3  29432  colinearalglem2  29491  axcgrid  29500  uvtx01vtx  29984  iscplgredg  30004  rgrusgrprc  30176  uspgr2wlkeq  30232  dfpth2  30320  clwlkclwwlk  30599  eupth2lem3lem6  30840  fusgr2wsp2nb  30941  nmorepnf  31376  blocnilem  31412  ubthlem1  31478  shscom  31927  pjpreeq  32006  spansncol  32176  cmcm2  32224  hodsi  32383  nmoprepnf  32475  nmfnrepnf  32488  pjssposi  32780  cvcon3  32892  mdsymlem8  33018  dmdsym  33021  disjunsn  33236  unipreima  33285  fmptcof2  33299  fdifsupp  33326  ressupprn  33331  1stpreima  33348  fpwrelmapffslem  33371  infxrge0gelb  33405  nndiffz1  33425  prodindf  33476  indf1ofs  33480  mgccnv  33607  pwrssmgc  33608  gsumwrd2dccatlem  33685  cntzun  33687  cntrval2  33779  isinftm  33789  domnprodeq0  33887  lindfpropd  33984  lindspropd  33985  unitprodclb  33991  lsmssass  34000  nsgmgc  34010  crngmxidl  34041  opprqusdrng  34064  qsfld  34069  ply1dg1rt  34159  selvply1rhmlemb  34198  psrmonmul  34229  finexttrb  34344  algextdeglem7  34402  ist0cld  34512  metidv  34571  metider  34573  pstmxmet  34576  xrge0iifiso  34614  aean  34924  brfae  34928  signsply0  35227  signsvfn  35258  reprinrn  35294  subfacp1lem3  36034  subfacp1lem5  36036  fmlafvel  36237  opelco3  36632  sscoid  36768  cgrcomr  36855  ofscom  36865  cgr3permute3  36905  cgr3permute1  36906  cgr3com  36911  colinearperm1  36920  colinearperm3  36921  outsideofcom  36986  naddle  37061  opnbnd  37206  filnetlem4  37262  finxpsuclem  38414  wl-equsald  38565  wl-equsaldv  38566  lindsadd  38630  poimirlem23  38655  broucube  38666  heicant  38667  itg2addnclem2  38684  ftc1anclem1  38705  ftc1anclem5  38709  ftc1anclem6  38710  areacirclem5  38724  areacirc  38725  caures  38788  cnpwstotbnd  38825  ismtyima  38831  rrnmet  38857  reheibor  38867  rngosn3  38952  ecxrn2  39434  brcosscnvcoss  39550  br1cosscnvxrn  39590  eqvrelth  39721  brpartspart  39902  lcvbr  40172  lkrsc  40248  lshpkrlem1  40261  opltcon3b  40355  cmt2N  40401  cmt3N  40402  cvrcon3b  40428  cvrcmp2  40435  cvlexchb2  40482  cvlatexchb2  40486  2llnmj  40711  4atlem3  40747  4atlem9  40754  4atlem10a  40755  4atlem11a  40758  4atlem12a  40761  4at2  40765  2lplnmj  40773  llnexchb2  41020  lautlt  41242  lautcvr  41243  lautco  41248  ltrnatb  41288  ltrneq2  41299  cdlemefrs29pre00  41546  cdlemefrs29cpre1  41549  cdleme32fva  41588  dibglbN  42317  dochsncom  42533  dochkrsat  42606  lspindp5  42921  mapdh8ab  42928  hdmapip0com  43068  quadfac  43349  dvdsexpb  43481  sn-ltmul2d  43631  fsuppind  43712  prjsprellsp  43733  lzenom  43875  rmxycomplete  44018  fzneg  44083  modabsdifz  44087  jm2.19  44094  pw2f1ocnv  44138  nadd1suc  44488  fzunt  44550  fzuntd  44551  fzunt1d  44552  fzuntgd  44553  sqrtcvallem1  44725  brtrclfv2  44821  rfovcnvf1od  45098  ntrclsfveq1  45154  ntrclsiso  45161  k0004lem2  45242  caofcan  45401  cocanss1  46018  rfcnpre1  46130  rfcnpre2  46142  ellimcabssub0  46723  liminfpnfuz  46920  xlimpnfxnegmnf2  46962  fperdvper  47023  vonvolmbl  47765  tmachlem-agreeprod  48041  readdcnnred  48467  resubcnnred  48468  cndivrenred  48470  submodaddmod  48511  minusmodnep2tmod  48523  requad2  48815  uhgrimisgrgric  49123  clnbgrgrim  49126  lco0  49633  lindslininds  49670  ltsubaddb  49720  ltsubsubb  49721  ltsubadd2b  49722  elbigolo1  49763  dig2bits  49820  prelrrx2bd  49920  rrx2pnedifcoorneorr  49924  mofeu  50053  sepnsepo  50132  lubeldm2d  50166  glbeldm2d  50167  cicpropdlem  50257  uptra  50425  uptr2a  50432  thincsect2  50697  thinccic  50700  isinito2lem  50727  postcposALT  50800  lanup  50918  ranup  50919  lmddu  50944