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  3835  pr1eqbg  4824  unisucg  6415  fimarab  6938  fvopab3g  6966  fvimacnvALT  7032  respreima  7041  fmptco  7104  fnnfpeq0  7155  cocan1  7269  cocan2  7270  caofidlcan  7694  ordsucelsuc  7800  ordsucsssuc  7801  fnsuppres  8173  smoword  8338  oaword  8516  omword  8537  om00el  8543  oeword  8557  nnaword  8594  nnmword  8600  eldifsucnn  8631  naddss1  8656  naddunif  8660  swoer  8705  erth  8728  brecop  8786  eceqoveq  8798  xpdom2  9041  pw2f1olem  9050  ixpfi2  9308  cantnfrescl  9636  ttrclselem2  9686  rankr1bg  9763  r1pwcl  9807  fseqenlem1  9984  alephord3  10038  alephdom2  10047  engch  10588  fpwwe2lem6  10596  fpwwe2lem8  10598  ltexpi  10862  ltapi  10863  ltmpi  10864  ltsonq  10929  ltmnq  10932  1idpr  10989  addcanpr  11006  axpre-ltadd  11127  axlttri  11252  subsub23  11433  leadd1  11653  ltsub1  11681  ltsub2  11682  leord1  11712  eqord1  11713  lemul1  12041  lediv1  12055  lt2mul2div  12068  lerec  12073  lediv2  12080  le2msq  12090  suprleub  12156  infregelb  12174  ofsubeq0  12190  ofsubge0  12192  avgle1  12429  avgle2  12430  cnref1o  12951  xleneg  13185  xnn0lem1lt  13211  xltadd1  13223  xsubge0  13228  xposdif  13229  xltmul1  13259  supxrleub  13293  infxrgelb  13303  iooneg  13439  iccneg  13440  iccsplit  13453  iccshftr  13454  iccshftl  13456  iccdil  13458  icccntr  13460  fzsplit2  13517  fzaddel  13526  fzrev  13555  predfz  13621  elfzo  13629  nelfzo  13632  fzon  13648  elfzom1b  13734  negmod0  13847  leexp2  14143  ltexp2r  14145  repswsymball  14751  repswsymballbi  14752  cjreb  15096  sqrtlt  15234  limsuplt  15452  o1lo1  15510  rlimresb  15538  lo1eq  15541  rlimeq  15542  o1eq  15543  isercoll  15641  efle  16093  tanaddlem  16141  nndivdvds  16238  moddvds  16240  modmulconst  16265  oddm1even  16320  ltoddhalfle  16338  bitsp1  16408  sadcaddlem  16434  sadadd  16444  sadass  16448  bitsshft  16452  smuval2  16459  smumul  16470  dvdssq  16544  phiprmpw  16753  eulerthlem2  16759  odzdvds  16773  pc2dvds  16857  1arith  16905  imasleval  17511  mreacs  17626  catpropd  17677  oppcsect  17747  funcres2b  17866  fthsect  17896  fthinv  17897  fucsect  17944  fucinv  17945  latnlemlt  18438  latnle  18439  ipole  18500  ipolt  18501  mgmpropd  18585  issubg3  19083  eqgid  19119  resghm2b  19173  conjghm  19188  ghmqusker  19226  gastacos  19249  resscntz  19272  cntzrec  19275  oppgsubm  19301  oppgsubg  19302  sylow3lem6  19569  lsmcom2  19592  lsmass  19606  ablsubsub23  19761  lsmcomx  19793  subgdmdprd  19973  opprsubrng  20475  opprsubrg  20509  lsslss  20874  lbspropd  21013  islbs2  21071  rspsn  21250  prmirred  21391  znfld  21477  lindfmm  21743  lindsmm  21744  lsslindf  21746  lsslinds  21747  islindf4  21754  psrbagconf1o  21845  gsumbagdiaglem  21846  mplmonmul  21950  basdif0  22847  neiptopreu  23027  neitr  23074  restlp  23077  cnrest2  23180  cnprest  23183  cnprest2  23184  lmss  23192  lmff  23195  ist1-2  23241  lpcls  23258  perfcls  23259  cmpfi  23302  hauseqlcld  23540  txlm  23542  txkgen  23546  xkopt  23549  idqtop  23600  tgqtop  23606  qtopcn  23608  uffix  23815  fmco  23855  flimrest  23877  lmflf  23899  txflf  23900  fclsrest  23918  cnpfcf  23935  tsmsgsum  24033  tsmsres  24038  tsmsf1o  24039  fmucndlem  24185  ismet2  24228  imasf1oxmet  24270  blres  24326  xmetec  24329  imasf1obl  24383  imasf1oxms  24384  prdsbl  24386  stdbdbl  24412  metrest  24419  metustsym  24450  blval2  24457  metuel2  24460  tngngp  24549  cnbl0  24668  cnblcld  24669  bl2ioo  24687  cncfcnvcn  24826  iihalf2  24835  icoopnst  24843  iocopnst  24844  icopnfcnv  24847  icopnfhmeo  24848  cphorthcom  25108  caucfil  25190  lmclim  25210  cmsss  25258  rrxmet  25315  volsup  25464  dyaddisjlem  25503  mbfeqalem1  25549  mbfeqalem2  25550  mbfeqa  25551  mbfmulc2lem  25555  mbfmax  25557  mbfposr  25560  ismbf3d  25562  mbfimaopnlem  25563  mbfaddlem  25568  mbfsup  25572  mbfinf  25573  0plef  25580  0pledm  25581  i1fmulclem  25610  i1fres  25613  i1fpos  25614  itg1climres  25622  mbfi1fseqlem4  25626  itg2mulclem  25654  itg2monolem1  25658  itg2cnlem1  25669  iblre  25702  iblcn  25707  itgeqa  25722  ellimc2  25785  limcflf  25789  dvreslem  25817  lhop1  25926  r1pid2  26074  ply1remlem  26077  fta1glem2  26081  ofmulrt  26196  plydiveu  26213  plyremlem  26219  quotcan  26224  ulmres  26304  cos11  26449  logleb  26519  argrege0  26527  logdivle  26538  efopn  26574  logccv  26579  cxplt  26610  cxple  26611  cxple2  26613  cxplt2  26614  cxplt3  26616  cxple3  26617  recxpf1lem  26645  logbleb  26700  logblt  26701  angrtmuld  26725  quad2  26756  atans2  26848  rlimcnp  26882  rlimcnp2  26883  rlimcxp  26891  sqff1o  27099  fsumvma2  27132  dchrptlem2  27183  lgsdilem  27242  lgsne0  27253  lgsqr  27269  lgsquadlem1  27298  lgsquadlem2  27299  m1lgs  27306  2lgslem1a  27309  2lgs  27325  dchrisum0lem1  27434  padicabv  27548  nosupinfsep  27651  oldlim  27805  newbday  27820  slelss  27827  sltadd2  27905  sleneg  27959  sltsub2  27988  sltsubsubbd  27994  slesubsubbd  27997  slesubsub2bd  27998  slesubsub3bd  27999  slemul2d  28084  slemul1d  28085  sltmulneg1d  28086  n0subs2  28261  trgcgrg  28449  colcom  28492  colrot1  28493  ishlg  28536  hlcomb  28537  hlbtwn  28545  lncom  28556  lnrot2  28558  israg  28631  perpcom  28647  hpgcom  28701  colopp  28703  iscgra  28743  isinag  28772  colinearalglem2  28841  axcgrid  28850  uvtx01vtx  29331  iscplgredg  29351  rgrusgrprc  29524  uspgr2wlkeq  29581  dfpth2  29666  clwlkclwwlk  29938  eupth2lem3lem6  30169  fusgr2wsp2nb  30270  nmorepnf  30704  blocnilem  30740  ubthlem1  30806  shscom  31255  pjpreeq  31334  spansncol  31504  cmcm2  31552  hodsi  31711  nmoprepnf  31803  nmfnrepnf  31816  pjssposi  32108  cvcon3  32220  mdsymlem8  32346  dmdsym  32349  disjunsn  32530  unipreima  32574  fmptcof2  32588  fdifsupp  32615  ressupprn  32620  1stpreima  32637  fpwrelmapffslem  32662  infxrge0gelb  32696  nndiffz1  32716  indpi1  32790  prodindf  32793  indf1ofs  32796  mgccnv  32932  pwrssmgc  32933  gsumwrd2dccatlem  33013  cntzun  33015  cntrval2  33135  isinftm  33142  qusxpid  33341  lindfpropd  33360  lindspropd  33361  unitprodclb  33367  lsmssass  33380  nsgmgc  33390  crngmxidl  33447  opprqusdrng  33471  qsfld  33476  ply1dg1rt  33555  finexttrb  33667  algextdeglem7  33720  ist0cld  33830  metidv  33889  metider  33891  pstmxmet  33894  xrge0iifiso  33932  aean  34241  brfae  34245  signsply0  34549  signsvfn  34580  reprinrn  34616  subfacp1lem3  35176  subfacp1lem5  35178  fmlafvel  35379  opelco3  35769  sscoid  35908  cgrcomr  35992  ofscom  36002  cgr3permute3  36042  cgr3permute1  36043  cgr3com  36048  colinearperm1  36057  colinearperm3  36058  outsideofcom  36123  opnbnd  36320  filnetlem4  36376  finxpsuclem  37392  wl-equsald  37534  wl-equsaldv  37535  lindsadd  37614  poimirlem23  37644  broucube  37655  heicant  37656  itg2addnclem2  37673  ftc1anclem1  37694  ftc1anclem5  37698  ftc1anclem6  37699  areacirclem5  37713  areacirc  37714  caures  37761  cnpwstotbnd  37798  ismtyima  37804  rrnmet  37830  reheibor  37840  rngosn3  37925  brcosscnvcoss  38432  br1cosscnvxrn  38472  eqvrelth  38609  brpartspart  38772  lcvbr  39021  lkrsc  39097  lshpkrlem1  39110  opltcon3b  39204  cmt2N  39250  cmt3N  39251  cvrcon3b  39277  cvrcmp2  39284  cvlexchb2  39331  cvlatexchb2  39335  2llnmj  39561  4atlem3  39597  4atlem9  39604  4atlem10a  39605  4atlem11a  39608  4atlem12a  39611  4at2  39615  2lplnmj  39623  llnexchb2  39870  lautlt  40092  lautcvr  40093  lautco  40098  ltrnatb  40138  ltrneq2  40149  cdlemefrs29pre00  40396  cdlemefrs29cpre1  40399  cdleme32fva  40438  dibglbN  41167  dochsncom  41383  dochkrsat  41456  lspindp5  41771  mapdh8ab  41778  hdmapip0com  41918  dvdsexpb  42330  sn-ltmul2d  42468  fsuppind  42585  prjsprellsp  42606  lzenom  42765  rmxycomplete  42913  fzneg  42978  modabsdifz  42982  jm2.19  42989  pw2f1ocnv  43033  nadd1suc  43388  fzunt  43451  fzuntd  43452  fzunt1d  43453  fzuntgd  43454  sqrtcvallem1  43627  brtrclfv2  43723  rfovcnvf1od  44000  ntrclsfveq1  44056  ntrclsiso  44063  k0004lem2  44144  caofcan  44319  rfcnpre1  45020  rfcnpre2  45032  ellimcabssub0  45622  liminfpnfuz  45821  xlimpnfxnegmnf2  45863  fperdvper  45924  vonvolmbl  46666  readdcnnred  47308  resubcnnred  47309  cndivrenred  47311  submodaddmod  47346  minusmodnep2tmod  47358  requad2  47628  uhgrimisgrgric  47935  clnbgrgrim  47938  lco0  48420  lindslininds  48457  ltsubaddb  48507  ltsubsubb  48508  ltsubadd2b  48509  elbigolo1  48550  dig2bits  48607  rrx2pnedifcoorneorr  48710  mofeu  48840  sepnsepo  48916  lubeldm2d  48950  glbeldm2d  48951  cicpropdlem  49042  uptra  49208  uptr2a  49215  thincsect2  49461  thinccic  49464  isinito2lem  49491  postcposALT  49561  lanup  49634  ranup  49635  lmddu  49660