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  6442  fvopab3g  6993  fvimacnvALT  7058  respreima  7067  fmptco  7129  fnnfpeq0  7178  cocan1  7292  cocan2  7293  ordsucelsuc  7814  ordsucsssuc  7815  fnsuppres  8181  smoword  8372  oaword  8555  omword  8576  om00el  8582  oeword  8596  nnaword  8633  nnmword  8639  eldifsucnn  8669  naddss1  8694  naddunif  8698  swoer  8739  erth  8758  brecop  8810  eceqoveq  8822  xpdom2  9073  pw2f1olem  9082  ixpfi2  9356  cantnfrescl  9677  ttrclselem2  9727  rankr1bg  9804  r1pwcl  9848  fseqenlem1  10025  alephord3  10079  alephdom2  10088  engch  10629  fpwwe2lem6  10637  fpwwe2lem8  10639  ltexpi  10903  ltapi  10904  ltmpi  10905  ltsonq  10970  ltmnq  10973  1idpr  11030  addcanpr  11047  axpre-ltadd  11168  axlttri  11292  subsub23  11472  leadd1  11689  ltsub1  11717  ltsub2  11718  leord1  11748  eqord1  11749  lemul1  12073  lediv1  12086  lt2mul2div  12099  lerec  12104  lediv2  12111  le2msq  12121  suprleub  12187  infregelb  12205  ofsubeq0  12216  ofsubge0  12218  avgle1  12459  avgle2  12460  cnref1o  12976  xleneg  13204  xnn0lem1lt  13230  xltadd1  13242  xsubge0  13247  xposdif  13248  xltmul1  13278  supxrleub  13312  infxrgelb  13321  iooneg  13455  iccneg  13456  iccsplit  13469  iccshftr  13470  iccshftl  13472  iccdil  13474  icccntr  13476  fzsplit2  13533  fzaddel  13542  fzrev  13571  predfz  13633  elfzo  13641  nelfzo  13644  fzon  13660  elfzom1b  13738  negmod0  13850  leexp2  14143  ltexp2r  14145  repswsymball  14736  repswsymballbi  14737  cjreb  15077  sqrtlt  15215  limsuplt  15430  o1lo1  15488  rlimresb  15516  lo1eq  15519  rlimeq  15520  o1eq  15521  isercoll  15621  efle  16068  tanaddlem  16116  nndivdvds  16213  moddvds  16215  modmulconst  16238  oddm1even  16293  ltoddhalfle  16311  bitsp1  16379  sadcaddlem  16405  sadadd  16415  sadass  16419  bitsshft  16423  smuval2  16430  smumul  16441  dvdssq  16511  phiprmpw  16716  eulerthlem2  16722  odzdvds  16735  pc2dvds  16819  1arith  16867  imasleval  17494  mreacs  17609  catpropd  17660  oppcsect  17732  funcres2b  17854  fthsect  17885  fthinv  17886  fucsect  17935  fucinv  17936  latnlemlt  18435  latnle  18436  ipole  18497  ipolt  18498  mgmpropd  18582  issubg3  19067  eqgid  19103  resghm2b  19155  conjghm  19170  gastacos  19222  resscntz  19245  cntzrec  19248  oppgsubm  19277  oppgsubg  19278  sylow3lem6  19548  lsmcom2  19571  lsmass  19585  ablsubsub23  19740  lsmcomx  19772  subgdmdprd  19952  opprsubrng  20455  opprsubrg  20491  lsslss  20804  lbspropd  20943  islbs2  21001  rspsn  21182  prmirred  21335  znfld  21427  lindfmm  21693  lindsmm  21694  lsslindf  21696  lsslinds  21697  islindf4  21704  psrbagconf1o  21800  psrbagconf1oOLD  21801  gsumbagdiaglemOLD  21802  gsumbagdiaglem  21805  mplmonmul  21903  basdif0  22777  neiptopreu  22958  neitr  23005  restlp  23008  cnrest2  23111  cnprest  23114  cnprest2  23115  lmss  23123  lmff  23126  ist1-2  23172  lpcls  23189  perfcls  23190  cmpfi  23233  hauseqlcld  23471  txlm  23473  txkgen  23477  xkopt  23480  idqtop  23531  tgqtop  23537  qtopcn  23539  uffix  23746  fmco  23786  flimrest  23808  lmflf  23830  txflf  23831  fclsrest  23849  cnpfcf  23866  tsmsgsum  23964  tsmsres  23969  tsmsf1o  23970  fmucndlem  24117  ismet2  24160  imasf1oxmet  24202  blres  24258  xmetec  24261  imasf1obl  24318  imasf1oxms  24319  prdsbl  24321  stdbdbl  24347  metrest  24354  metustsym  24385  blval2  24392  metuel2  24395  tngngp  24492  cnbl0  24611  cnblcld  24612  bl2ioo  24629  cncfcnvcn  24767  iihalf2  24776  icoopnst  24784  iocopnst  24785  icopnfcnv  24788  icopnfhmeo  24789  cphorthcom  25050  caucfil  25132  lmclim  25152  cmsss  25200  rrxmet  25257  volsup  25406  dyaddisjlem  25445  mbfeqalem1  25491  mbfeqalem2  25492  mbfeqa  25493  mbfmulc2lem  25497  mbfmax  25499  mbfposr  25502  ismbf3d  25504  mbfimaopnlem  25505  mbfaddlem  25510  mbfsup  25514  mbfinf  25515  0plef  25522  0pledm  25523  i1fmulclem  25553  i1fres  25556  i1fpos  25557  itg1climres  25565  mbfi1fseqlem4  25569  itg2mulclem  25597  itg2monolem1  25601  itg2cnlem1  25612  iblre  25644  iblcn  25649  itgeqa  25664  ellimc2  25727  limcflf  25731  dvreslem  25759  lhop1  25868  ply1remlem  26019  fta1glem2  26023  ofmulrt  26135  plydiveu  26151  plyremlem  26157  quotcan  26162  ulmres  26240  cos11  26383  logleb  26452  argrege0  26460  logdivle  26471  efopn  26507  logccv  26512  cxplt  26543  cxple  26544  cxple2  26546  cxplt2  26547  cxplt3  26549  cxple3  26550  recxpf1lem  26578  logbleb  26630  logblt  26631  angrtmuld  26655  quad2  26686  atans2  26778  rlimcnp  26812  rlimcnp2  26813  rlimcxp  26821  sqff1o  27029  fsumvma2  27062  dchrptlem2  27113  lgsdilem  27172  lgsne0  27183  lgsqr  27199  lgsquadlem1  27228  lgsquadlem2  27229  m1lgs  27236  2lgslem1a  27239  2lgs  27255  dchrisum0lem1  27364  padicabv  27478  nosupinfsep  27580  oldlim  27728  newbday  27743  slelss  27749  sltadd2  27823  sleneg  27873  sltsub2  27900  sltsubsubbd  27906  slesubsubbd  27909  slesubsub2bd  27910  slesubsub3bd  27911  slemul2d  27989  slemul1d  27990  sltmulneg1d  27991  trgcgrg  28201  colcom  28244  colrot1  28245  ishlg  28288  hlcomb  28289  hlbtwn  28297  lncom  28308  lnrot2  28310  israg  28383  perpcom  28399  hpgcom  28453  colopp  28455  iscgra  28495  isinag  28524  colinearalglem2  28600  axcgrid  28609  uvtx01vtx  29089  iscplgredg  29109  rgrusgrprc  29281  uspgr2wlkeq  29338  clwlkclwwlk  29690  eupth2lem3lem6  29921  fusgr2wsp2nb  30022  nmorepnf  30456  blocnilem  30492  ubthlem1  30558  shscom  31007  pjpreeq  31086  spansncol  31256  cmcm2  31304  hodsi  31463  nmoprepnf  31555  nmfnrepnf  31568  pjssposi  31860  cvcon3  31972  mdsymlem8  32098  dmdsym  32101  disjunsn  32260  fimarab  32303  unipreima  32304  fmptcof2  32317  ressupprn  32347  1stpreima  32363  fpwrelmapffslem  32392  infxrge0gelb  32414  nndiffz1  32432  mgccnv  32604  pwrssmgc  32605  cntzun  32650  isinftm  32765  qusxpid  32917  lindfpropd  32940  lindspropd  32941  lsmssass  32954  nsgmgc  32965  ghmqusker  32974  crngmxidl  33027  opprqusdrng  33049  qsfld  33054  finexttrb  33197  algextdeglem7  33236  ist0cld  33279  metidv  33338  metider  33340  pstmxmet  33343  xrge0iifiso  33381  indpi1  33484  prodindf  33487  indf1ofs  33490  aean  33708  brfae  33712  signsply0  34028  signsvfn  34059  reprinrn  34096  subfacp1lem3  34639  subfacp1lem5  34641  fmlafvel  34842  opelco3  35218  sscoid  35357  cgrcomr  35441  ofscom  35451  cgr3permute3  35491  cgr3permute1  35492  cgr3com  35497  colinearperm1  35506  colinearperm3  35507  outsideofcom  35572  opnbnd  35677  filnetlem4  35733  finxpsuclem  36745  wl-equsald  36875  lindsadd  36948  poimirlem23  36978  broucube  36989  heicant  36990  itg2addnclem2  37007  ftc1anclem1  37028  ftc1anclem5  37032  ftc1anclem6  37033  areacirclem5  37047  areacirc  37048  caures  37095  cnpwstotbnd  37132  ismtyima  37138  rrnmet  37164  reheibor  37174  rngosn3  37259  brcosscnvcoss  37771  br1cosscnvxrn  37811  eqvrelth  37948  brpartspart  38110  lcvbr  38358  lkrsc  38434  lshpkrlem1  38447  opltcon3b  38541  cmt2N  38587  cmt3N  38588  cvrcon3b  38614  cvrcmp2  38621  cvlexchb2  38668  cvlatexchb2  38672  2llnmj  38898  4atlem3  38934  4atlem9  38941  4atlem10a  38942  4atlem11a  38945  4atlem12a  38948  4at2  38952  2lplnmj  38960  llnexchb2  39207  lautlt  39429  lautcvr  39430  lautco  39435  ltrnatb  39475  ltrneq2  39486  cdlemefrs29pre00  39733  cdlemefrs29cpre1  39736  cdleme32fva  39775  dibglbN  40504  dochsncom  40720  dochkrsat  40793  lspindp5  41108  mapdh8ab  41115  hdmapip0com  41255  fsuppind  41628  dvdsexpb  41699  sn-ltmul2d  41800  prjsprellsp  41819  lzenom  41974  rmxycomplete  42122  fzneg  42187  modabsdifz  42191  jm2.19  42198  pw2f1ocnv  42242  nadd1suc  42608  fzunt  42672  fzuntd  42673  fzunt1d  42674  fzuntgd  42675  sqrtcvallem1  42848  brtrclfv2  42944  rfovcnvf1od  43221  ntrclsfveq1  43277  ntrclsiso  43284  k0004lem2  43365  caofcan  43548  rfcnpre1  44169  rfcnpre2  44181  ellimcabssub0  44795  liminfpnfuz  44994  xlimpnfxnegmnf2  45036  fperdvper  45097  vonvolmbl  45839  readdcnnred  46473  resubcnnred  46474  cndivrenred  46476  requad2  46753  lco0  47273  lindslininds  47310  ltsubaddb  47360  ltsubsubb  47361  ltsubadd2b  47362  elbigolo1  47408  dig2bits  47465  rrx2pnedifcoorneorr  47568  mofeu  47679  sepnsepo  47721  lubeldm2d  47756  glbeldm2d  47757  thincsect2  47843  thinccic  47846  postcposALT  47866