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  3820  pr1eqbg  4820  unisucg  6442  fimarab  6956  fvopab3g  6985  fvimacnvALT  7053  respreima  7062  fmptco  7127  fnnfpeq0  7180  cocan1  7296  cocan2  7297  caofidlcan  7720  ordsucelsuc  7822  ordsucsssuc  7823  fnsuppres  8193  smoword  8359  oaword  8540  omword  8561  om00el  8567  oeword  8582  nnaword  8619  nnmword  8625  eldifsucnn  8656  naddss1  8682  naddunif  8686  swoer  8732  erth  8755  brecop  8814  eceqoveq  8826  xpdom2  9074  pw2f1olem  9083  ixpfi2  9321  cantnfrescl  9659  ttrclselem2  9709  rankr1bg  9789  r1pwcl  9833  fseqenlem1  10031  alephord3  10085  alephdom2  10094  engch  10641  fpwwe2lem6  10649  fpwwe2lem8  10651  ltexpi  10915  ltapi  10916  ltmpi  10917  ltsonq  10982  ltmnq  10985  1idpr  11042  addcanpr  11059  axpre-ltadd  11180  axlttri  11309  subsub23  11490  leadd1  11710  ltsub1  11738  ltsub2  11739  leord1  11769  eqord1  11770  lemul1  12095  lediv1  12108  lt2mul2div  12121  lerec  12126  lediv2  12133  le2msq  12143  suprleub  12209  infregelb  12227  ofsubeq0  12243  ofsubge0  12245  indpi1  12260  avgle1  12512  avgle2  12513  cnref1o  13039  xleneg  13274  xnn0lem1lt  13300  xltadd1  13312  xsubge0  13317  xposdif  13318  xltmul1  13348  supxrleub  13382  infxrgelb  13392  iooneg  13528  iccneg  13529  iccsplit  13542  iccshftr  13543  iccshftl  13545  iccdil  13547  icccntr  13549  fzsplit2  13608  fzaddel  13617  fzrev  13646  predfz  13712  elfzo  13720  nelfzo  13724  fzon  13740  elfzom1b  13826  negmod0  13943  leexp2  14239  ltexp2r  14241  repswsymball  14854  repswsymballbi  14855  cjreb  15214  sqrtlt  15352  limsuplt  15570  o1lo1  15628  rlimresb  15656  lo1eq  15659  rlimeq  15660  o1eq  15661  isercoll  15759  efle  16212  tanaddlem  16260  nndivdvds  16357  moddvds  16359  modmulconst  16384  oddm1even  16439  ltoddhalfle  16457  bitsp1  16527  sadcaddlem  16553  sadadd  16563  sadass  16567  bitsshft  16571  smuval2  16578  smumul  16589  dvdssq  16663  phiprmpw  16873  eulerthlem2  16879  odzdvds  16893  pc2dvds  16977  1arith  17025  imasleval  17633  mreacs  17752  catpropd  17803  oppcsect  17873  funcres2b  17992  fthsect  18022  fthinv  18023  fucsect  18070  fucinv  18071  latnlemlt  18566  latnle  18567  ipole  18628  ipolt  18629  mgmpropd  18749  issubg3  19274  eqgid  19311  qusxpid  19314  resghm2b  19367  conjghm  19382  ghmqusker  19420  gastacos  19443  resscntz  19466  cntzrec  19469  oppgsubm  19495  oppgsubg  19496  sylow3lem6  19765  lsmcom2  19788  lsmass  19802  ablsubsub23  19957  lsmcomx  19989  subgdmdprd  20169  opprsubrng  20727  opprsubrg  20761  lsslss  21151  lbspropd  21289  islbs2  21347  rspsn  21570  prmirred  21693  znfld  21779  lindfmm  22046  lindsmm  22047  lsslindf  22049  lsslinds  22050  islindf4  22057  psrbagconf1o  22150  gsumbagdiaglem  22152  mplmonmul  22258  basdif0  23184  neiptopreu  23364  neitr  23411  restlp  23414  cnrest2  23517  cnprest  23520  cnprest2  23521  lmss  23529  lmff  23532  ist1-2  23578  lpcls  23595  perfcls  23596  cmpfi  23639  hauseqlcld  23878  txlm  23880  txkgen  23884  xkopt  23887  idqtop  23938  tgqtop  23944  qtopcn  23946  uffix  24153  fmco  24193  flimrest  24215  lmflf  24237  txflf  24238  fclsrest  24256  cnpfcf  24273  tsmsgsum  24371  tsmsres  24376  tsmsf1o  24377  fmucndlem  24522  ismet2  24565  imasf1oxmet  24607  blres  24663  xmetec  24666  imasf1obl  24720  imasf1oxms  24721  prdsbl  24723  stdbdbl  24749  metrest  24756  metustsym  24787  blval2  24794  metuel2  24797  tngngp  24886  cnbl0  25005  cnblcld  25006  bl2ioo  25024  cncfcnvcn  25159  iihalf2  25167  icoopnst  25173  iocopnst  25174  icopnfcnv  25176  icopnfhmeo  25177  cphorthcom  25435  caucfil  25517  lmclim  25537  cmsss  25585  rrxmet  25642  volsup  25790  dyaddisjlem  25829  mbfeqalem1  25875  mbfeqalem2  25876  mbfeqa  25877  mbfmulc2lem  25881  mbfmax  25883  mbfposr  25886  ismbf3d  25888  mbfimaopnlem  25889  mbfaddlem  25894  mbfsup  25898  mbfinf  25899  0plef  25906  0pledm  25907  i1fmulclem  25936  i1fres  25939  i1fpos  25940  itg1climres  25948  mbfi1fseqlem4  25952  itg2mulclem  25980  itg2monolem1  25984  itg2cnlem1  25995  iblre  26028  iblcn  26033  itgeqa  26048  ellimc2  26111  limcflf  26115  dvreslem  26143  lhop1  26248  r1pid2  26394  ply1remlem  26397  fta1glem2  26401  ofmulrt  26516  plydiveu  26535  plyremlem  26541  rnplynfin  26546  quotcan  26548  ulmres  26631  cos11  26778  logleb  26848  argrege0  26856  logdivle  26867  efopn  26903  logccv  26908  cxplt  26939  cxple  26940  cxple2  26942  cxplt2  26943  cxplt3  26945  cxple3  26946  recxpf1lem  26974  logbleb  27028  logblt  27029  angrtmuld  27053  quad2  27084  atans2  27176  rlimcnp  27210  rlimcnp2  27211  rlimcxp  27218  sqff1o  27426  fsumvma2  27458  dchrptlem2  27509  lgsdilem  27568  lgsne0  27579  lgsqr  27595  lgsquadlem1  27624  lgsquadlem2  27625  m1lgs  27632  2lgslem1a  27635  2lgs  27651  dchrisum0lem1  27760  padicabv  27874  nosupinfsep  27976  oldlim  28160  newbday  28175  leslss  28182  ltadds2  28264  lenegs  28319  ltsubs2  28350  ltsubsubsbd  28356  lesubsubsbd  28359  lesubsubs2bd  28360  lesubsubs3bd  28361  lesubsd  28369  lemuls2d  28447  lemuls1d  28448  ltmulnegs1d  28449  onles  28541  n0subs2  28637  bdaypw2bnd  28738  bdayfinbndlem1  28740  trgcgrg  28865  colcom  28908  colrot1  28909  ishlg  28955  hlcomb  28956  hlbtwn  28964  lncom  28977  lnrot2  28979  israg  29059  perpcom  29075  hpgcom  29132  colopp  29134  plngcplem  29150  iscgra  29203  isinag  29244  dfprlng3  29313  colinearalglem2  29372  axcgrid  29381  uvtx01vtx  29865  iscplgredg  29885  rgrusgrprc  30057  uspgr2wlkeq  30113  dfpth2  30201  clwlkclwwlk  30480  eupth2lem3lem6  30721  fusgr2wsp2nb  30822  nmorepnf  31257  blocnilem  31293  ubthlem1  31359  shscom  31808  pjpreeq  31887  spansncol  32057  cmcm2  32105  hodsi  32264  nmoprepnf  32356  nmfnrepnf  32369  pjssposi  32661  cvcon3  32773  mdsymlem8  32899  dmdsym  32902  disjunsn  33075  unipreima  33124  fmptcof2  33138  fdifsupp  33165  ressupprn  33170  1stpreima  33187  fpwrelmapffslem  33211  infxrge0gelb  33245  nndiffz1  33265  prodindf  33316  indf1ofs  33320  mgccnv  33447  pwrssmgc  33448  gsumwrd2dccatlem  33525  cntzun  33527  cntrval2  33619  isinftm  33629  domnprodeq0  33727  lindfpropd  33823  lindspropd  33824  unitprodclb  33830  lsmssass  33839  nsgmgc  33849  crngmxidl  33880  opprqusdrng  33903  qsfld  33908  ply1dg1rt  33998  selvply1rhmlemb  34037  psrmonmul  34068  finexttrb  34183  algextdeglem7  34241  ist0cld  34351  metidv  34410  metider  34412  pstmxmet  34415  xrge0iifiso  34453  aean  34763  brfae  34767  signsply0  35067  signsvfn  35098  reprinrn  35134  subfacp1lem3  35769  subfacp1lem5  35771  fmlafvel  35972  opelco3  36362  sscoid  36498  cgrcomr  36585  ofscom  36595  cgr3permute3  36635  cgr3permute1  36636  cgr3com  36641  colinearperm1  36650  colinearperm3  36651  outsideofcom  36716  naddle  36807  opnbnd  36952  filnetlem4  37008  finxpsuclem  38159  wl-equsald  38310  wl-equsaldv  38311  lindsadd  38375  poimirlem23  38400  broucube  38411  heicant  38412  itg2addnclem2  38429  ftc1anclem1  38450  ftc1anclem5  38454  ftc1anclem6  38455  areacirclem5  38469  areacirc  38470  caures  38518  cnpwstotbnd  38555  ismtyima  38561  rrnmet  38587  reheibor  38597  rngosn3  38682  ecxrn2  39164  brcosscnvcoss  39280  br1cosscnvxrn  39320  eqvrelth  39451  brpartspart  39632  lcvbr  39902  lkrsc  39978  lshpkrlem1  39991  opltcon3b  40085  cmt2N  40131  cmt3N  40132  cvrcon3b  40158  cvrcmp2  40165  cvlexchb2  40212  cvlatexchb2  40216  2llnmj  40441  4atlem3  40477  4atlem9  40484  4atlem10a  40485  4atlem11a  40488  4atlem12a  40491  4at2  40495  2lplnmj  40503  llnexchb2  40750  lautlt  40972  lautcvr  40973  lautco  40978  ltrnatb  41018  ltrneq2  41029  cdlemefrs29pre00  41276  cdlemefrs29cpre1  41279  cdleme32fva  41318  dibglbN  42047  dochsncom  42263  dochkrsat  42336  lspindp5  42651  mapdh8ab  42658  hdmapip0com  42798  quadfac  43079  dvdsexpb  43218  sn-ltmul2d  43369  fsuppind  43444  prjsprellsp  43465  lzenom  43623  rmxycomplete  43766  fzneg  43831  modabsdifz  43835  jm2.19  43842  pw2f1ocnv  43886  nadd1suc  44241  fzunt  44303  fzuntd  44304  fzunt1d  44305  fzuntgd  44306  sqrtcvallem1  44479  brtrclfv2  44575  rfovcnvf1od  44852  ntrclsfveq1  44908  ntrclsiso  44915  k0004lem2  44996  caofcan  45155  rfcnpre1  45861  rfcnpre2  45873  ellimcabssub0  46455  liminfpnfuz  46652  xlimpnfxnegmnf2  46694  fperdvper  46755  vonvolmbl  47497  tmachlem-agreeprod  47773  readdcnnred  48199  resubcnnred  48200  cndivrenred  48202  submodaddmod  48243  minusmodnep2tmod  48255  requad2  48547  uhgrimisgrgric  48855  clnbgrgrim  48858  lco0  49365  lindslininds  49402  ltsubaddb  49452  ltsubsubb  49453  ltsubadd2b  49454  elbigolo1  49495  dig2bits  49552  rrx2pnedifcoorneorr  49655  mofeu  49784  sepnsepo  49858  lubeldm2d  49892  glbeldm2d  49893  cicpropdlem  49983  uptra  50149  uptr2a  50156  thincsect2  50402  thinccic  50405  isinito2lem  50432  postcposALT  50502  lanup  50575  ranup  50576  lmddu  50601