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 ⊢ (𝜑 → (𝜃 ↔ 𝜏))

Syntax hints:   → wi 4   ↔ wb 209

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 210

This theorem is referenced by:  sbccomlem  3823  pr1eqbg  4823  unisucg  6443  fimarab  6957  fvopab3g  6986  fvimacnvALT  7054  respreima  7063  fmptco  7127  fnnfpeq0  7178  cocan1  7291  cocan2  7292  caofidlcan  7714  ordsucelsuc  7819  ordsucsssuc  7820  fnsuppres  8188  smoword  8354  oaword  8535  omword  8556  om00el  8562  oeword  8577  nnaword  8614  nnmword  8620  eldifsucnn  8651  naddss1  8677  naddunif  8681  swoer  8727  erth  8750  brecop  8809  eceqoveq  8821  xpdom2  9061  pw2f1olem  9070  ixpfi2  9308  cantnfrescl  9646  ttrclselem2  9696  rankr1bg  9776  r1pwcl  9820  fseqenlem1  10009  alephord3  10063  alephdom2  10072  engch  10614  fpwwe2lem6  10622  fpwwe2lem8  10624  ltexpi  10888  ltapi  10889  ltmpi  10890  ltsonq  10955  ltmnq  10958  1idpr  11015  addcanpr  11032  axpre-ltadd  11153  axlttri  11282  subsub23  11463  leadd1  11683  ltsub1  11711  ltsub2  11712  leord1  11742  eqord1  11743  lemul1  12068  lediv1  12081  lt2mul2div  12094  lerec  12099  lediv2  12106  le2msq  12116  suprleub  12182  infregelb  12200  ofsubeq0  12216  ofsubge0  12218  indpi1  12233  avgle1  12485  avgle2  12486  cnref1o  13010  xleneg  13245  xnn0lem1lt  13271  xltadd1  13283  xsubge0  13288  xposdif  13289  xltmul1  13319  supxrleub  13353  infxrgelb  13363  iooneg  13499  iccneg  13500  iccsplit  13513  iccshftr  13514  iccshftl  13516  iccdil  13518  icccntr  13520  fzsplit2  13579  fzaddel  13588  fzrev  13617  predfz  13683  elfzo  13691  nelfzo  13695  fzon  13711  elfzom1b  13797  negmod0  13913  leexp2  14209  ltexp2r  14211  repswsymball  14818  repswsymballbi  14819  cjreb  15176  sqrtlt  15314  limsuplt  15532  o1lo1  15590  rlimresb  15618  lo1eq  15621  rlimeq  15622  o1eq  15623  isercoll  15721  efle  16175  tanaddlem  16223  nndivdvds  16320  moddvds  16322  modmulconst  16347  oddm1even  16402  ltoddhalfle  16420  bitsp1  16490  sadcaddlem  16516  sadadd  16526  sadass  16530  bitsshft  16534  smuval2  16541  smumul  16552  dvdssq  16626  phiprmpw  16836  eulerthlem2  16842  odzdvds  16856  pc2dvds  16940  1arith  16988  imasleval  17596  mreacs  17715  catpropd  17766  oppcsect  17836  funcres2b  17955  fthsect  17985  fthinv  17986  fucsect  18033  fucinv  18034  latnlemlt  18529  latnle  18530  ipole  18591  ipolt  18592  mgmpropd  18710  issubg3  19212  eqgid  19249  qusxpid  19252  resghm2b  19305  conjghm  19320  ghmqusker  19358  gastacos  19381  resscntz  19404  cntzrec  19407  oppgsubm  19433  oppgsubg  19434  sylow3lem6  19703  lsmcom2  19726  lsmass  19740  ablsubsub23  19895  lsmcomx  19927  subgdmdprd  20107  opprsubrng  20645  opprsubrg  20679  lsslss  21063  lbspropd  21201  islbs2  21259  rspsn  21482  prmirred  21605  znfld  21691  lindfmm  21958  lindsmm  21959  lsslindf  21961  lsslinds  21962  islindf4  21969  psrbagconf1o  22060  gsumbagdiaglem  22062  mplmonmul  22168  basdif0  23091  neiptopreu  23271  neitr  23318  restlp  23321  cnrest2  23424  cnprest  23427  cnprest2  23428  lmss  23436  lmff  23439  ist1-2  23485  lpcls  23502  perfcls  23503  cmpfi  23546  hauseqlcld  23784  txlm  23786  txkgen  23790  xkopt  23793  idqtop  23844  tgqtop  23850  qtopcn  23852  uffix  24059  fmco  24099  flimrest  24121  lmflf  24143  txflf  24144  fclsrest  24162  cnpfcf  24179  tsmsgsum  24277  tsmsres  24282  tsmsf1o  24283  fmucndlem  24428  ismet2  24471  imasf1oxmet  24513  blres  24569  xmetec  24572  imasf1obl  24626  imasf1oxms  24627  prdsbl  24629  stdbdbl  24655  metrest  24662  metustsym  24693  blval2  24700  metuel2  24703  tngngp  24792  cnbl0  24911  cnblcld  24912  bl2ioo  24930  cncfcnvcn  25065  iihalf2  25073  icoopnst  25079  iocopnst  25080  icopnfcnv  25082  icopnfhmeo  25083  cphorthcom  25341  caucfil  25423  lmclim  25443  cmsss  25491  rrxmet  25548  volsup  25696  dyaddisjlem  25735  mbfeqalem1  25781  mbfeqalem2  25782  mbfeqa  25783  mbfmulc2lem  25787  mbfmax  25789  mbfposr  25792  ismbf3d  25794  mbfimaopnlem  25795  mbfaddlem  25800  mbfsup  25804  mbfinf  25805  0plef  25812  0pledm  25813  i1fmulclem  25842  i1fres  25845  i1fpos  25846  itg1climres  25854  mbfi1fseqlem4  25858  itg2mulclem  25886  itg2monolem1  25890  itg2cnlem1  25901  iblre  25934  iblcn  25939  itgeqa  25954  ellimc2  26017  limcflf  26021  dvreslem  26049  lhop1  26154  r1pid2  26300  ply1remlem  26303  fta1glem2  26307  ofmulrt  26421  plydiveu  26440  plyremlem  26446  quotcan  26451  ulmres  26532  cos11  26679  logleb  26749  argrege0  26757  logdivle  26768  efopn  26804  logccv  26809  cxplt  26840  cxple  26841  cxple2  26843  cxplt2  26844  cxplt3  26846  cxple3  26847  recxpf1lem  26875  logbleb  26929  logblt  26930  angrtmuld  26954  quad2  26985  atans2  27077  rlimcnp  27111  rlimcnp2  27112  rlimcxp  27119  sqff1o  27327  fsumvma2  27359  dchrptlem2  27410  lgsdilem  27469  lgsne0  27480  lgsqr  27496  lgsquadlem1  27525  lgsquadlem2  27526  m1lgs  27533  2lgslem1a  27536  2lgs  27552  dchrisum0lem1  27661  padicabv  27775  nosupinfsep  27877  oldlim  28061  newbday  28076  leslss  28083  ltadds2  28165  lenegs  28220  ltsubs2  28251  ltsubsubsbd  28257  lesubsubsbd  28260  lesubsubs2bd  28261  lesubsubs3bd  28262  lesubsd  28270  lemuls2d  28348  lemuls1d  28349  ltmulnegs1d  28350  onles  28442  n0subs2  28538  bdaypw2bnd  28639  bdayfinbndlem1  28641  trgcgrg  28765  colcom  28808  colrot1  28809  ishlg  28855  hlcomb  28856  hlbtwn  28864  lncom  28876  lnrot2  28878  israg  28958  perpcom  28974  hpgcom  29030  colopp  29032  plngcplem  29048  iscgra  29101  isinag  29136  dfprlng3  29179  colinearalglem2  29238  axcgrid  29247  uvtx01vtx  29728  iscplgredg  29748  rgrusgrprc  29920  uspgr2wlkeq  29976  dfpth2  30059  clwlkclwwlk  30334  eupth2lem3lem6  30565  fusgr2wsp2nb  30666  nmorepnf  31101  blocnilem  31137  ubthlem1  31203  shscom  31652  pjpreeq  31731  spansncol  31901  cmcm2  31949  hodsi  32108  nmoprepnf  32200  nmfnrepnf  32213  pjssposi  32505  cvcon3  32617  mdsymlem8  32743  dmdsym  32746  disjunsn  32920  unipreima  32969  fmptcof2  32983  fdifsupp  33011  ressupprn  33016  1stpreima  33033  fpwrelmapffslem  33058  infxrge0gelb  33092  nndiffz1  33112  prodindf  33163  indf1ofs  33167  mgccnv  33300  pwrssmgc  33301  gsumwrd2dccatlem  33378  cntzun  33380  cntrval2  33472  isinftm  33482  domnprodeq0  33580  lindfpropd  33676  lindspropd  33677  unitprodclb  33683  lsmssass  33692  nsgmgc  33702  crngmxidl  33733  opprqusdrng  33756  qsfld  33761  ply1dg1rt  33851  selvply1rhmlemb  33890  psrmonmul  33921  finexttrb  34036  algextdeglem7  34094  ist0cld  34204  metidv  34263  metider  34265  pstmxmet  34268  xrge0iifiso  34306  aean  34615  brfae  34619  signsply0  34919  signsvfn  34950  reprinrn  34986  subfacp1lem3  35655  subfacp1lem5  35657  fmlafvel  35858  opelco3  36248  sscoid  36384  cgrcomr  36470  ofscom  36480  cgr3permute3  36520  cgr3permute1  36521  cgr3com  36526  colinearperm1  36535  colinearperm3  36536  outsideofcom  36601  naddle  36677  opnbnd  36817  filnetlem4  36873  finxpsuclem  38024  wl-equsald  38175  wl-equsaldv  38176  lindsadd  38245  poimirlem23  38275  broucube  38286  heicant  38287  itg2addnclem2  38304  ftc1anclem1  38325  ftc1anclem5  38329  ftc1anclem6  38330  areacirclem5  38344  areacirc  38345  caures  38392  cnpwstotbnd  38429  ismtyima  38435  rrnmet  38461  reheibor  38471  rngosn3  38556  ecxrn2  39038  brcosscnvcoss  39154  br1cosscnvxrn  39194  eqvrelth  39325  brpartspart  39506  lcvbr  39776  lkrsc  39852  lshpkrlem1  39865  opltcon3b  39959  cmt2N  40005  cmt3N  40006  cvrcon3b  40032  cvrcmp2  40039  cvlexchb2  40086  cvlatexchb2  40090  2llnmj  40315  4atlem3  40351  4atlem9  40358  4atlem10a  40359  4atlem11a  40362  4atlem12a  40365  4at2  40369  2lplnmj  40377  llnexchb2  40624  lautlt  40846  lautcvr  40847  lautco  40852  ltrnatb  40892  ltrneq2  40903  cdlemefrs29pre00  41150  cdlemefrs29cpre1  41153  cdleme32fva  41192  dibglbN  41921  dochsncom  42137  dochkrsat  42210  lspindp5  42525  mapdh8ab  42532  hdmapip0com  42672  quadfac  42953  dvdsexpb  43077  sn-ltmul2d  43228  fsuppind  43305  prjsprellsp  43326  lzenom  43484  rmxycomplete  43627  fzneg  43692  modabsdifz  43696  jm2.19  43703  pw2f1ocnv  43747  nadd1suc  44102  fzunt  44164  fzuntd  44165  fzunt1d  44166  fzuntgd  44167  sqrtcvallem1  44340  brtrclfv2  44436  rfovcnvf1od  44713  ntrclsfveq1  44769  ntrclsiso  44776  k0004lem2  44857  caofcan  45016  rfcnpre1  45722  rfcnpre2  45734  ellimcabssub0  46316  liminfpnfuz  46513  xlimpnfxnegmnf2  46555  fperdvper  46616  vonvolmbl  47358  readdcnnred  48023  resubcnnred  48024  cndivrenred  48026  submodaddmod  48067  minusmodnep2tmod  48079  requad2  48371  uhgrimisgrgric  48679  clnbgrgrim  48682  lco0  49190  lindslininds  49227  ltsubaddb  49277  ltsubsubb  49278  ltsubadd2b  49279  elbigolo1  49320  dig2bits  49377  rrx2pnedifcoorneorr  49480  mofeu  49609  sepnsepo  49685  lubeldm2d  49719  glbeldm2d  49720  cicpropdlem  49810  uptra  49976  uptr2a  49983  thincsect2  50229  thinccic  50232  isinito2lem  50259  postcposALT  50329  lanup  50402  ranup  50403  lmddu  50428