Theorem 3imtr4d 294

Description: More general version of 3imtr4i 292. Useful for converting conditional definitions in a formula. (Contributed by NM, 26-Oct-1995.)

Hypotheses

Ref	Expression
3imtr4d.1	⊢ (𝜑 → (𝜓 → 𝜒))
3imtr4d.2	⊢ (𝜑 → (𝜃 ↔ 𝜓))
3imtr4d.3	⊢ (𝜑 → (𝜏 ↔ 𝜒))

Assertion

Ref	Expression
3imtr4d	⊢ (𝜑 → (𝜃 → 𝜏))

Proof of Theorem 3imtr4d

Step	Hyp	Ref	Expression
1		3imtr4d.2	. 2 ⊢ (𝜑 → (𝜃 ↔ 𝜓))
2		3imtr4d.1	. . 3 ⊢ (𝜑 → (𝜓 → 𝜒))
3		3imtr4d.3	. . 3 ⊢ (𝜑 → (𝜏 ↔ 𝜒))
4	2, 3	sylibrd 259	. 2 ⊢ (𝜑 → (𝜓 → 𝜏))
5	1, 4	sylbid 240	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:  rmosn  4678  unielrel  6240  predtrss  6288  fvrnressn  7116  fconst5  7162  soisores  7283  caofrss  7671  caoftrn  7673  f1o2ndf1  8074  oaord  8484  omord2  8504  omcan  8506  oeord  8526  oecan  8527  nnaord  8557  nnmord  8570  omsmo  8596  pmss12g  8819  cantnf  9614  pm54.43  9925  ttukeylem2  10432  axlttrn  11217  axltadd  11218  axmulgt0  11219  axsup  11220  ltadd2  11249  ltord1  11675  recex  11781  ltmul1  12003  lt2msq  12039  nnge1  12185  zltp1le  12553  uzss  12786  eluzp1m1  12789  prodge0rd  13026  ixxssixx  13287  zesq  14161  pfxccatin12lem3  14667  swrdccat3blem  14674  relexpsucnnr  14960  climrlim2  15482  rlimres  15493  climshftlem  15509  lo1add  15562  lo1mul  15563  rlimsqzlem  15584  lo1le  15587  isercolllem2  15601  isercoll  15603  climsup  15605  cvgcmp  15751  climcndslem1  15784  dvds1lem  16206  sumodd  16327  rprpwr  16498  algcvg  16515  eucalgcvga  16525  rpexp12i  16663  crth  16717  pc2dvds  16819  pcmpt  16832  prmpwdvds  16844  1arith  16867  vdwlem2  16922  vdwlem6  16926  vdwlem8  16928  ercpbl  17482  initoid  17937  termoid  17938  ipopos  18471  insubm  18755  subginv  19075  symggrp  19341  f1otrspeq  19388  lsmless1x  19585  lsmless2x  19586  dprdss  19972  rngpropd  20121  dvdsunit  20327  irredrmul  20375  isdrngd  20710  isdrngdOLD  20712  lspextmo  21020  rngqiprngimf1lem  21261  domnchr  21499  zntoslem  21523  evlseu  22050  mat2pmatf1  22685  tgss  22924  neips  23069  opnnei  23076  lpss3  23100  ssrest  23132  t1t0  23304  kgen2ss  23511  isfild  23814  fgss  23829  fgss2  23830  cnpflf2  23956  fclsss1  23978  fclsss2  23979  tgpt0  24075  tsmsxp  24111  prdsxmslem2  24485  ngptgp  24592  nghmcn  24701  qdensere  24725  evth  24926  nmhmcn  25088  tcphcph  25205  caussi  25265  equivcfil  25267  rrxmvallem  25372  ivthlem2  25421  ovollb2lem  25457  ovolunlem1  25466  volun  25514  ioombl1lem4  25530  volsup2  25574  volcn  25575  ismbf3d  25623  itg2mulclem  25715  cpnord  25905  lhop1  25987  aaliou3lem2  26319  ulmclm  26364  ulmss  26374  abelth  26419  cosord  26508  efif1olem4  26522  argimgt0  26589  logdivlt  26598  cxploglim  26956  dvdssqf  27116  mumullem1  27157  mumullem2  27158  bposlem6  27268  lgsdchr  27334  gausslemma2dlem1a  27344  m1lgs  27367  chtppilim  27454  lestr  27742  lestric  27748  madebdayim  27896  madebdaylemold  27906  ltslpss  27916  om2noseqf1o  28309  zsoring  28417  bdaypw2n0bndlem  28471  bdayfin  28495  ax5seg  29023  axpasch  29026  axlowdimlem16  29042  axeuclid  29048  axcontlem4  29052  usgr1v0e  29411  nb3gr2nb  29469  cplgr1v  29515  finsumvtxdg2size  29636  usgr2pthlem  29848  clwwlknwwlksn  30125  erclwwlknsym  30157  erclwwlkntr  30158  frgr3vlem1  30360  3vfriswmgrlem  30364  numclwwlk5  30475  minvecolem5  30969  ocsh  31371  shless  31447  leopadd  32220  leopmuli  32221  leopmul2i  32223  leoptr  32225  spansncv2  32381  mdsl0  32398  ssdmd1  32401  cvdmd  32425  cdj3i  32529  uzssico  32875  expgt0b  32908  eqgvscpbl  33443  qusvscpbl  33444  cmpcref  34028  acycgrsubgr  35374  cvmliftmolem1  35497  satffunlem2lem2  35622  mrsubff1  35730  msubff1  35772  lediv2aALT  35893  cgr3tr4  36268  colinearxfr  36291  lineext  36292  brsegle  36324  seglecgr12im  36326  segletr  36330  colinbtwnle  36334  outsideoftr  36345  lineelsb2  36364  ivthALT  36551  tailfb  36593  poimirlem29  37900  itg2addnclem  37922  itg2addnclem3  37924  itg2addnc  37925  incsequz  37999  mettrifi  38008  ismtycnv  38053  bfplem1  38073  ghomco  38142  rngoisocnv  38232  keridl  38283  dmncan1  38327  ax12indalem  39321  ax12inda2ALT  39322  omllaw4  39622  cmtcomlemN  39624  cvlexch2  39705  cvlatexch2  39713  cvrexch  39796  atexchltN  39817  3atlem5  39863  lplnribN  39927  linepsubN  40128  paddss1  40193  paddss2  40194  pmapjoin  40228  pmapjat1  40229  cdleme36a  40836  dib2dim  41619  dih2dimbALTN  41621  djhcvat42  41791  dihjatcclem4  41797  dihjat1lem  41804  lcfrlem6  41923  hlhillcs  42334  oexpreposd  42692  mulgt0b1d  42842  mullt0b1d  42853  pell1234qrmulcl  43212  pell14qrss1234  43213  pell14qrmulcl  43220  pell14qrreccl  43221  pell1qrss14  43225  monotoddzzfi  43299  oddcomabszz  43301  omabs2  43689  omcl3g  43691  tfsconcat0b  43703  naddwordnexlem4  43758  climinf  45966  2ffzoeq  47687  iccpartgt  47787  pgnbgreunbgrlem1  48473  pgnbgreunbgrlem4  48479  upwlkwlk  48499  uspgrsprf1  48507  rrx2xpref1o  49078  itschlc0yqe  49120  resipos  49334