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 206

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 207

This theorem is referenced by:  sbccomlem  3877  pr1eqbg  4861  unisucg  6463  fimarab  6982  fvopab3g  7010  fvimacnvALT  7076  respreima  7085  fmptco  7148  fnnfpeq0  7197  cocan1  7310  cocan2  7311  ordsucelsuc  7841  ordsucsssuc  7842  fnsuppres  8214  smoword  8404  oaword  8585  omword  8606  om00el  8612  oeword  8626  nnaword  8663  nnmword  8669  eldifsucnn  8700  naddss1  8725  naddunif  8729  swoer  8774  erth  8794  brecop  8848  eceqoveq  8860  xpdom2  9105  pw2f1olem  9114  ixpfi2  9387  cantnfrescl  9713  ttrclselem2  9763  rankr1bg  9840  r1pwcl  9884  fseqenlem1  10061  alephord3  10115  alephdom2  10124  engch  10665  fpwwe2lem6  10673  fpwwe2lem8  10675  ltexpi  10939  ltapi  10940  ltmpi  10941  ltsonq  11006  ltmnq  11009  1idpr  11066  addcanpr  11083  axpre-ltadd  11204  axlttri  11329  subsub23  11510  leadd1  11728  ltsub1  11756  ltsub2  11757  leord1  11787  eqord1  11788  lemul1  12116  lediv1  12130  lt2mul2div  12143  lerec  12148  lediv2  12155  le2msq  12165  suprleub  12231  infregelb  12249  ofsubeq0  12260  ofsubge0  12262  avgle1  12503  avgle2  12504  cnref1o  13024  xleneg  13256  xnn0lem1lt  13282  xltadd1  13294  xsubge0  13299  xposdif  13300  xltmul1  13330  supxrleub  13364  infxrgelb  13373  iooneg  13507  iccneg  13508  iccsplit  13521  iccshftr  13522  iccshftl  13524  iccdil  13526  icccntr  13528  fzsplit2  13585  fzaddel  13594  fzrev  13623  predfz  13689  elfzo  13697  nelfzo  13700  fzon  13716  elfzom1b  13801  negmod0  13914  leexp2  14207  ltexp2r  14209  repswsymball  14813  repswsymballbi  14814  cjreb  15158  sqrtlt  15296  limsuplt  15511  o1lo1  15569  rlimresb  15597  lo1eq  15600  rlimeq  15601  o1eq  15602  isercoll  15700  efle  16150  tanaddlem  16198  nndivdvds  16295  moddvds  16297  modmulconst  16321  oddm1even  16376  ltoddhalfle  16394  bitsp1  16464  sadcaddlem  16490  sadadd  16500  sadass  16504  bitsshft  16508  smuval2  16515  smumul  16526  dvdssq  16600  phiprmpw  16809  eulerthlem2  16815  odzdvds  16828  pc2dvds  16912  1arith  16960  imasleval  17587  mreacs  17702  catpropd  17753  oppcsect  17825  funcres2b  17947  fthsect  17978  fthinv  17979  fucsect  18028  fucinv  18029  latnlemlt  18529  latnle  18530  ipole  18591  ipolt  18592  mgmpropd  18676  issubg3  19174  eqgid  19210  resghm2b  19264  conjghm  19279  ghmqusker  19317  gastacos  19340  resscntz  19363  cntzrec  19366  oppgsubm  19395  oppgsubg  19396  sylow3lem6  19664  lsmcom2  19687  lsmass  19701  ablsubsub23  19856  lsmcomx  19888  subgdmdprd  20068  opprsubrng  20575  opprsubrg  20609  lsslss  20976  lbspropd  21115  islbs2  21173  rspsn  21360  prmirred  21502  znfld  21596  lindfmm  21864  lindsmm  21865  lsslindf  21867  lsslinds  21868  islindf4  21875  psrbagconf1o  21966  gsumbagdiaglem  21967  mplmonmul  22071  basdif0  22975  neiptopreu  23156  neitr  23203  restlp  23206  cnrest2  23309  cnprest  23312  cnprest2  23313  lmss  23321  lmff  23324  ist1-2  23370  lpcls  23387  perfcls  23388  cmpfi  23431  hauseqlcld  23669  txlm  23671  txkgen  23675  xkopt  23678  idqtop  23729  tgqtop  23735  qtopcn  23737  uffix  23944  fmco  23984  flimrest  24006  lmflf  24028  txflf  24029  fclsrest  24047  cnpfcf  24064  tsmsgsum  24162  tsmsres  24167  tsmsf1o  24168  fmucndlem  24315  ismet2  24358  imasf1oxmet  24400  blres  24456  xmetec  24459  imasf1obl  24516  imasf1oxms  24517  prdsbl  24519  stdbdbl  24545  metrest  24552  metustsym  24583  blval2  24590  metuel2  24593  tngngp  24690  cnbl0  24809  cnblcld  24810  bl2ioo  24827  cncfcnvcn  24965  iihalf2  24974  icoopnst  24982  iocopnst  24983  icopnfcnv  24986  icopnfhmeo  24987  cphorthcom  25248  caucfil  25330  lmclim  25350  cmsss  25398  rrxmet  25455  volsup  25604  dyaddisjlem  25643  mbfeqalem1  25689  mbfeqalem2  25690  mbfeqa  25691  mbfmulc2lem  25695  mbfmax  25697  mbfposr  25700  ismbf3d  25702  mbfimaopnlem  25703  mbfaddlem  25708  mbfsup  25712  mbfinf  25713  0plef  25720  0pledm  25721  i1fmulclem  25751  i1fres  25754  i1fpos  25755  itg1climres  25763  mbfi1fseqlem4  25767  itg2mulclem  25795  itg2monolem1  25799  itg2cnlem1  25810  iblre  25843  iblcn  25848  itgeqa  25863  ellimc2  25926  limcflf  25930  dvreslem  25958  lhop1  26067  r1pid2  26215  ply1remlem  26218  fta1glem2  26222  ofmulrt  26337  plydiveu  26354  plyremlem  26360  quotcan  26365  ulmres  26445  cos11  26589  logleb  26659  argrege0  26667  logdivle  26678  efopn  26714  logccv  26719  cxplt  26750  cxple  26751  cxple2  26753  cxplt2  26754  cxplt3  26756  cxple3  26757  recxpf1lem  26785  logbleb  26840  logblt  26841  angrtmuld  26865  quad2  26896  atans2  26988  rlimcnp  27022  rlimcnp2  27023  rlimcxp  27031  sqff1o  27239  fsumvma2  27272  dchrptlem2  27323  lgsdilem  27382  lgsne0  27393  lgsqr  27409  lgsquadlem1  27438  lgsquadlem2  27439  m1lgs  27446  2lgslem1a  27449  2lgs  27465  dchrisum0lem1  27574  padicabv  27688  nosupinfsep  27791  oldlim  27939  newbday  27954  slelss  27960  sltadd2  28038  sleneg  28092  sltsub2  28121  sltsubsubbd  28127  slesubsubbd  28130  slesubsub2bd  28131  slesubsub3bd  28132  slemul2d  28214  slemul1d  28215  sltmulneg1d  28216  trgcgrg  28537  colcom  28580  colrot1  28581  ishlg  28624  hlcomb  28625  hlbtwn  28633  lncom  28644  lnrot2  28646  israg  28719  perpcom  28735  hpgcom  28789  colopp  28791  iscgra  28831  isinag  28860  colinearalglem2  28936  axcgrid  28945  uvtx01vtx  29428  iscplgredg  29448  rgrusgrprc  29621  uspgr2wlkeq  29678  clwlkclwwlk  30030  eupth2lem3lem6  30261  fusgr2wsp2nb  30362  nmorepnf  30796  blocnilem  30832  ubthlem1  30898  shscom  31347  pjpreeq  31426  spansncol  31596  cmcm2  31644  hodsi  31803  nmoprepnf  31895  nmfnrepnf  31908  pjssposi  32200  cvcon3  32312  mdsymlem8  32438  dmdsym  32441  disjunsn  32613  unipreima  32659  fmptcof2  32673  fdifsupp  32699  ressupprn  32704  1stpreima  32721  fpwrelmapffslem  32749  infxrge0gelb  32776  nndiffz1  32794  mgccnv  32973  pwrssmgc  32974  gsumwrd2dccatlem  33051  cntzun  33053  isinftm  33170  qusxpid  33370  lindfpropd  33389  lindspropd  33390  unitprodclb  33396  lsmssass  33409  nsgmgc  33419  crngmxidl  33476  opprqusdrng  33500  qsfld  33505  ply1dg1rt  33583  finexttrb  33689  algextdeglem7  33728  ist0cld  33793  metidv  33852  metider  33854  pstmxmet  33857  xrge0iifiso  33895  indpi1  34000  prodindf  34003  indf1ofs  34006  aean  34224  brfae  34228  signsply0  34544  signsvfn  34575  reprinrn  34611  subfacp1lem3  35166  subfacp1lem5  35168  fmlafvel  35369  opelco3  35755  sscoid  35894  cgrcomr  35978  ofscom  35988  cgr3permute3  36028  cgr3permute1  36029  cgr3com  36034  colinearperm1  36043  colinearperm3  36044  outsideofcom  36109  opnbnd  36307  filnetlem4  36363  finxpsuclem  37379  wl-equsald  37519  wl-equsaldv  37520  lindsadd  37599  poimirlem23  37629  broucube  37640  heicant  37641  itg2addnclem2  37658  ftc1anclem1  37679  ftc1anclem5  37683  ftc1anclem6  37684  areacirclem5  37698  areacirc  37699  caures  37746  cnpwstotbnd  37783  ismtyima  37789  rrnmet  37815  reheibor  37825  rngosn3  37910  brcosscnvcoss  38415  br1cosscnvxrn  38455  eqvrelth  38592  brpartspart  38754  lcvbr  39002  lkrsc  39078  lshpkrlem1  39091  opltcon3b  39185  cmt2N  39231  cmt3N  39232  cvrcon3b  39258  cvrcmp2  39265  cvlexchb2  39312  cvlatexchb2  39316  2llnmj  39542  4atlem3  39578  4atlem9  39585  4atlem10a  39586  4atlem11a  39589  4atlem12a  39592  4at2  39596  2lplnmj  39604  llnexchb2  39851  lautlt  40073  lautcvr  40074  lautco  40079  ltrnatb  40119  ltrneq2  40130  cdlemefrs29pre00  40377  cdlemefrs29cpre1  40380  cdleme32fva  40419  dibglbN  41148  dochsncom  41364  dochkrsat  41437  lspindp5  41752  mapdh8ab  41759  hdmapip0com  41899  dvdsexpb  42348  sn-ltmul2d  42467  fsuppind  42576  prjsprellsp  42597  lzenom  42757  rmxycomplete  42905  fzneg  42970  modabsdifz  42974  jm2.19  42981  pw2f1ocnv  43025  nadd1suc  43381  fzunt  43444  fzuntd  43445  fzunt1d  43446  fzuntgd  43447  sqrtcvallem1  43620  brtrclfv2  43716  rfovcnvf1od  43993  ntrclsfveq1  44049  ntrclsiso  44056  k0004lem2  44137  caofcan  44318  rfcnpre1  44956  rfcnpre2  44968  ellimcabssub0  45572  liminfpnfuz  45771  xlimpnfxnegmnf2  45813  fperdvper  45874  vonvolmbl  46616  readdcnnred  47252  resubcnnred  47253  cndivrenred  47255  submodaddmod  47280  minusmodnep2tmod  47292  requad2  47547  uhgrimisgrgric  47836  clnbgrgrim  47839  lco0  48272  lindslininds  48309  ltsubaddb  48359  ltsubsubb  48360  ltsubadd2b  48361  elbigolo1  48406  dig2bits  48463  rrx2pnedifcoorneorr  48566  mofeu  48677  sepnsepo  48719  lubeldm2d  48754  glbeldm2d  48755  thincsect2  48858  thinccic  48861  postcposALT  48883