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  3817  pr1eqbg  4817  unisucg  6436  fimarab  6951  fvopab3g  6980  fvimacnvALT  7048  respreima  7057  fmptco  7122  fnnfpeq0  7175  cocan1  7291  cocan2  7292  caofidlcan  7720  ordsucelsuc  7822  ordsucsssuc  7823  fnsuppres  8192  smoword  8358  oaword  8541  omword  8562  om00el  8568  oeword  8583  nnaword  8620  nnmword  8626  eldifsucnn  8657  naddss1  8683  naddunif  8687  swoer  8733  erth  8756  brecop  8815  eceqoveq  8827  xpdom2  9075  pw2f1olem  9084  ixpfi2  9323  cantnfrescl  9661  ttrclselem2  9711  rankr1bg  9793  r1pwcl  9842  fseqenlem1  10084  alephord3  10138  alephdom2  10147  engch  10694  fpwwe2lem6  10702  fpwwe2lem8  10704  ltexpi  10968  ltapi  10969  ltmpi  10970  ltsonq  11035  ltmnq  11038  1idpr  11095  addcanpr  11112  axpre-ltadd  11233  axlttri  11362  subsub23  11543  leadd1  11765  ltsub1  11793  ltsub2  11794  leord1  11824  eqord1  11825  lemul1  12150  lediv1  12163  lt2mul2div  12176  lerec  12181  lediv2  12188  le2msq  12198  suprleub  12264  infregelb  12282  ofsubeq0  12298  ofsubge0  12300  indpi1  12315  avgle1  12567  avgle2  12568  cnref1o  13094  xleneg  13329  xnn0lem1lt  13355  xltadd1  13367  xsubge0  13372  xposdif  13373  xltmul1  13403  supxrleub  13437  infxrgelb  13447  iooneg  13583  iccneg  13584  iccsplit  13597  iccshftr  13598  iccshftl  13600  iccdil  13602  icccntr  13604  fzsplit2  13663  fzaddel  13672  fzrev  13701  predfz  13767  elfzo  13775  nelfzo  13779  fzon  13795  elfzom1b  13881  negmod0  13998  leexp2  14294  ltexp2r  14296  repswsymball  14910  repswsymballbi  14911  cjreb  15270  sqrtlt  15408  limsuplt  15626  o1lo1  15684  rlimresb  15712  lo1eq  15715  rlimeq  15716  o1eq  15717  isercoll  15815  efle  16266  tanaddlem  16314  nndivdvds  16411  moddvds  16413  modmulconst  16438  oddm1even  16493  ltoddhalfle  16511  bitsp1  16581  sadcaddlem  16607  sadadd  16617  sadass  16621  bitsshft  16625  smuval2  16632  smumul  16643  dvdssq  16722  phiprmpw  16933  eulerthlem2  16939  odzdvds  16953  pc2dvds  17037  1arith  17085  imasleval  17693  mreacs  17812  catpropd  17863  oppcsect  17933  funcres2b  18052  fthsect  18082  fthinv  18083  fucsect  18130  fucinv  18131  latnlemlt  18626  latnle  18627  ipole  18688  ipolt  18689  mgmpropd  18809  issubg3  19335  eqgid  19372  qusxpid  19375  resghm2b  19428  conjghm  19443  ghmqusker  19481  gastacos  19504  resscntz  19527  cntzrec  19530  oppgsubm  19556  oppgsubg  19557  sylow3lem6  19826  lsmcom2  19849  lsmass  19863  ablsubsub23  20018  lsmcomx  20050  subgdmdprd  20230  opprsubrng  20791  opprsubrg  20825  lsslss  21216  lbspropd  21354  islbs2  21412  rspsn  21637  prmirred  21760  znfld  21846  lindfmm  22113  lindsmm  22114  lsslindf  22116  lsslinds  22117  islindf4  22124  psrbagconf1o  22217  gsumbagdiaglem  22219  mplmonmul  22325  basdif0  23251  neiptopreu  23431  neitr  23478  restlp  23481  cnrest2  23584  cnprest  23587  cnprest2  23588  lmss  23596  lmff  23599  ist1-2  23645  lpcls  23662  perfcls  23663  cmpfi  23706  hauseqlcld  23945  txlm  23947  txkgen  23951  xkopt  23954  idqtop  24005  tgqtop  24011  qtopcn  24013  uffix  24220  fmco  24260  flimrest  24282  lmflf  24304  txflf  24305  fclsrest  24323  cnpfcf  24340  tsmsgsum  24438  tsmsres  24443  tsmsf1o  24444  fmucndlem  24589  ismet2  24632  imasf1oxmet  24674  blres  24730  xmetec  24733  imasf1obl  24787  imasf1oxms  24788  prdsbl  24790  stdbdbl  24816  metrest  24823  metustsym  24854  blval2  24861  metuel2  24864  tngngp  24953  cnbl0  25072  cnblcld  25073  bl2ioo  25091  cncfcnvcn  25226  iihalf2  25234  icoopnst  25240  iocopnst  25241  icopnfcnv  25243  icopnfhmeo  25244  cphorthcom  25502  caucfil  25584  lmclim  25604  cmsss  25652  rrxmet  25709  volsup  25857  dyaddisjlem  25896  mbfeqalem1  25942  mbfeqalem2  25943  mbfeqa  25944  mbfmulc2lem  25948  mbfmax  25950  mbfposr  25953  ismbf3d  25955  mbfimaopnlem  25956  mbfaddlem  25961  mbfsup  25965  mbfinf  25966  0plef  25973  0pledm  25974  i1fmulclem  26003  i1fres  26006  i1fpos  26007  itg1climres  26015  mbfi1fseqlem4  26019  itg2mulclem  26047  itg2monolem1  26051  itg2cnlem1  26062  iblre  26094  iblcn  26099  itgeqa  26114  ellimc2  26177  limcflf  26181  dvreslem  26209  lhop1  26314  r1pid2  26460  ply1remlem  26463  fta1glem2  26467  ofmulrt  26582  plydiveu  26601  plyremlem  26607  rnplynfin  26612  quotcan  26614  ulmres  26697  cos11  26843  logleb  26913  argrege0  26921  logdivle  26932  efopn  26968  logccv  26973  cxplt  27004  cxple  27005  cxple2  27007  cxplt2  27008  cxplt3  27010  cxple3  27011  recxpf1lem  27039  logbleb  27093  logblt  27094  angrtmuld  27118  quad2  27149  atans2  27241  rlimcnp  27275  rlimcnp2  27276  rlimcxp  27283  sqff1o  27491  fsumvma2  27523  dchrptlem2  27574  lgsdilem  27633  lgsne0  27644  lgsqr  27660  lgsquadlem1  27689  lgsquadlem2  27690  m1lgs  27697  2lgslem1a  27700  2lgs  27716  dchrisum0lem1  27825  padicabv  27939  nosupinfsep  28071  oldlim  28255  newbday  28270  leslss  28277  ltadds2  28359  lenegs  28414  ltsubs2  28445  ltsubsubsbd  28451  lesubsubsbd  28454  lesubsubs2bd  28455  lesubsubs3bd  28456  lesubsd  28464  lemuls2d  28542  lemuls1d  28543  ltmulnegs1d  28544  onles  28636  n0subs2  28732  bdaypw2bnd  28833  bdayfinbndlem1  28835  trgcgrg  28960  colcom  29003  colrot1  29004  ishlg  29050  hlcomb  29051  hlbtwn  29059  lncom  29072  lnrot2  29074  israg  29154  perpcom  29170  hpgcom  29227  colopp  29229  plngcplem  29245  iscgra  29298  isinag  29339  dfprlng3  29408  colinearalglem2  29467  axcgrid  29476  uvtx01vtx  29960  iscplgredg  29980  rgrusgrprc  30152  uspgr2wlkeq  30208  dfpth2  30296  clwlkclwwlk  30575  eupth2lem3lem6  30816  fusgr2wsp2nb  30917  nmorepnf  31352  blocnilem  31388  ubthlem1  31454  shscom  31903  pjpreeq  31982  spansncol  32152  cmcm2  32200  hodsi  32359  nmoprepnf  32451  nmfnrepnf  32464  pjssposi  32756  cvcon3  32868  mdsymlem8  32994  dmdsym  32997  disjunsn  33170  unipreima  33219  fmptcof2  33233  fdifsupp  33260  ressupprn  33265  1stpreima  33282  fpwrelmapffslem  33306  infxrge0gelb  33340  nndiffz1  33360  prodindf  33411  indf1ofs  33415  mgccnv  33542  pwrssmgc  33543  gsumwrd2dccatlem  33620  cntzun  33622  cntrval2  33714  isinftm  33724  domnprodeq0  33822  lindfpropd  33919  lindspropd  33920  unitprodclb  33926  lsmssass  33935  nsgmgc  33945  crngmxidl  33976  opprqusdrng  33999  qsfld  34004  ply1dg1rt  34094  selvply1rhmlemb  34133  psrmonmul  34164  finexttrb  34279  algextdeglem7  34337  ist0cld  34447  metidv  34506  metider  34508  pstmxmet  34511  xrge0iifiso  34549  aean  34859  brfae  34863  signsply0  35163  signsvfn  35194  reprinrn  35230  subfacp1lem3  35916  subfacp1lem5  35918  fmlafvel  36119  opelco3  36509  sscoid  36645  cgrcomr  36732  ofscom  36742  cgr3permute3  36782  cgr3permute1  36783  cgr3com  36788  colinearperm1  36797  colinearperm3  36798  outsideofcom  36863  naddle  36938  opnbnd  37083  filnetlem4  37139  finxpsuclem  38288  wl-equsald  38439  wl-equsaldv  38440  lindsadd  38504  poimirlem23  38529  broucube  38540  heicant  38541  itg2addnclem2  38558  ftc1anclem1  38579  ftc1anclem5  38583  ftc1anclem6  38584  areacirclem5  38598  areacirc  38599  caures  38662  cnpwstotbnd  38699  ismtyima  38705  rrnmet  38731  reheibor  38741  rngosn3  38826  ecxrn2  39308  brcosscnvcoss  39424  br1cosscnvxrn  39464  eqvrelth  39595  brpartspart  39776  lcvbr  40046  lkrsc  40122  lshpkrlem1  40135  opltcon3b  40229  cmt2N  40275  cmt3N  40276  cvrcon3b  40302  cvrcmp2  40309  cvlexchb2  40356  cvlatexchb2  40360  2llnmj  40585  4atlem3  40621  4atlem9  40628  4atlem10a  40629  4atlem11a  40632  4atlem12a  40635  4at2  40639  2lplnmj  40647  llnexchb2  40894  lautlt  41116  lautcvr  41117  lautco  41122  ltrnatb  41162  ltrneq2  41173  cdlemefrs29pre00  41420  cdlemefrs29cpre1  41423  cdleme32fva  41462  dibglbN  42191  dochsncom  42407  dochkrsat  42480  lspindp5  42795  mapdh8ab  42802  hdmapip0com  42942  quadfac  43223  dvdsexpb  43355  sn-ltmul2d  43505  fsuppind  43580  prjsprellsp  43601  lzenom  43734  rmxycomplete  43877  fzneg  43942  modabsdifz  43946  jm2.19  43953  pw2f1ocnv  43997  nadd1suc  44352  fzunt  44414  fzuntd  44415  fzunt1d  44416  fzuntgd  44417  sqrtcvallem1  44590  brtrclfv2  44686  rfovcnvf1od  44963  ntrclsfveq1  45019  ntrclsiso  45026  k0004lem2  45107  caofcan  45266  rfcnpre1  45979  rfcnpre2  45991  ellimcabssub0  46573  liminfpnfuz  46770  xlimpnfxnegmnf2  46812  fperdvper  46873  vonvolmbl  47615  tmachlem-agreeprod  47891  readdcnnred  48317  resubcnnred  48318  cndivrenred  48320  submodaddmod  48361  minusmodnep2tmod  48373  requad2  48665  uhgrimisgrgric  48973  clnbgrgrim  48976  lco0  49483  lindslininds  49520  ltsubaddb  49570  ltsubsubb  49571  ltsubadd2b  49572  elbigolo1  49613  dig2bits  49670  rrx2pnedifcoorneorr  49773  mofeu  49902  sepnsepo  49976  lubeldm2d  50010  glbeldm2d  50011  cicpropdlem  50101  uptra  50267  uptr2a  50274  thincsect2  50520  thinccic  50523  isinito2lem  50550  postcposALT  50620  lanup  50693  ranup  50694  lmddu  50719