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  4724  unielrel  6296  predtrss  6345  fvrnressn  7181  fconst5  7226  soisores  7347  caofrss  7735  caoftrn  7737  f1o2ndf1  8146  oaord  8584  omord2  8604  omcan  8606  oeord  8625  oecan  8626  nnaord  8656  nnmord  8669  omsmo  8695  pmss12g  8908  cantnf  9731  pm54.43  10039  ttukeylem2  10548  axlttrn  11331  axltadd  11332  axmulgt0  11333  axsup  11334  ltadd2  11363  ltord1  11787  recex  11893  ltmul1  12115  lt2msq  12151  nnge1  12292  zltp1le  12665  uzss  12899  eluzp1m1  12902  prodge0rd  13140  ixxssixx  13398  zesq  14262  pfxccatin12lem3  14767  swrdccat3blem  14774  relexpsucnnr  15061  climrlim2  15580  rlimres  15591  climshftlem  15607  lo1add  15660  lo1mul  15661  rlimsqzlem  15682  lo1le  15685  isercolllem2  15699  isercoll  15701  climsup  15703  cvgcmp  15849  climcndslem1  15882  dvds1lem  16302  sumodd  16422  rprpwr  16593  algcvg  16610  eucalgcvga  16620  rpexp12i  16758  crth  16812  pc2dvds  16913  pcmpt  16926  prmpwdvds  16938  1arith  16961  vdwlem2  17016  vdwlem6  17020  vdwlem8  17022  ercpbl  17596  initoid  18055  termoid  18056  ipopos  18594  insubm  18844  subginv  19164  symggrp  19433  f1otrspeq  19480  lsmless1x  19677  lsmless2x  19678  dprdss  20064  rngpropd  20192  dvdsunit  20396  irredrmul  20444  isdrngd  20782  isdrngdOLD  20784  lspextmo  21073  rngqiprngimf1lem  21322  domnchr  21565  zntoslem  21593  evlseu  22125  mat2pmatf1  22751  tgss  22991  neips  23137  opnnei  23144  lpss3  23168  ssrest  23200  t1t0  23372  kgen2ss  23579  isfild  23882  fgss  23897  fgss2  23898  cnpflf2  24024  fclsss1  24046  fclsss2  24047  tgpt0  24143  tsmsxp  24179  prdsxmslem2  24558  ngptgp  24665  nghmcn  24782  qdensere  24806  evth  25005  nmhmcn  25167  tcphcph  25285  caussi  25345  equivcfil  25347  rrxmvallem  25452  ivthlem2  25501  ovollb2lem  25537  ovolunlem1  25546  volun  25594  ioombl1lem4  25610  volsup2  25654  volcn  25655  ismbf3d  25703  itg2mulclem  25796  cpnord  25986  lhop1  26068  aaliou3lem2  26400  ulmclm  26445  ulmss  26455  abelth  26500  cosord  26588  efif1olem4  26602  argimgt0  26669  logdivlt  26678  cxploglim  27036  dvdssqf  27196  mumullem1  27237  mumullem2  27238  bposlem6  27348  lgsdchr  27414  gausslemma2dlem1a  27424  m1lgs  27447  chtppilim  27534  sletr  27818  sletric  27824  madebdayim  27941  madebdaylemold  27951  sltlpss  27960  om2noseqf1o  28322  ax5seg  28968  axpasch  28971  axlowdimlem16  28987  axeuclid  28993  axcontlem4  28997  usgr1v0e  29358  nb3gr2nb  29416  cplgr1v  29462  finsumvtxdg2size  29583  usgr2pthlem  29796  clwwlknwwlksn  30067  erclwwlknsym  30099  erclwwlkntr  30100  frgr3vlem1  30302  3vfriswmgrlem  30306  numclwwlk5  30417  minvecolem5  30910  ocsh  31312  shless  31388  leopadd  32161  leopmuli  32162  leopmul2i  32164  leoptr  32166  spansncv2  32322  mdsl0  32339  ssdmd1  32342  cvdmd  32366  cdj3i  32470  uzssico  32793  expgt0b  32823  eqgvscpbl  33358  qusvscpbl  33359  cmpcref  33811  acycgrsubgr  35143  cvmliftmolem1  35266  satffunlem2lem2  35391  mrsubff1  35499  msubff1  35541  lediv2aALT  35662  cgr3tr4  36034  colinearxfr  36057  lineext  36058  brsegle  36090  seglecgr12im  36092  segletr  36096  colinbtwnle  36100  outsideoftr  36111  lineelsb2  36130  ivthALT  36318  tailfb  36360  poimirlem29  37636  itg2addnclem  37658  itg2addnclem3  37660  itg2addnc  37661  incsequz  37735  mettrifi  37744  ismtycnv  37789  bfplem1  37809  ghomco  37878  rngoisocnv  37968  keridl  38019  dmncan1  38063  ax12indalem  38927  ax12inda2ALT  38928  omllaw4  39228  cmtcomlemN  39230  cvlexch2  39311  cvlatexch2  39319  cvrexch  39403  atexchltN  39424  3atlem5  39470  lplnribN  39534  linepsubN  39735  paddss1  39800  paddss2  39801  pmapjoin  39835  pmapjat1  39836  cdleme36a  40443  dib2dim  41226  dih2dimbALTN  41228  djhcvat42  41398  dihjatcclem4  41404  dihjat1lem  41411  lcfrlem6  41530  hlhillcs  41945  oexpreposd  42336  mulgt0b2d  42467  pell1234qrmulcl  42843  pell14qrss1234  42844  pell14qrmulcl  42851  pell14qrreccl  42852  pell1qrss14  42856  monotoddzzfi  42931  oddcomabszz  42933  omabs2  43322  omcl3g  43324  tfsconcat0b  43336  naddwordnexlem4  43391  climinf  45562  2ffzoeq  47277  iccpartgt  47352  upwlkwlk  47983  uspgrsprf1  47991  rrx2xpref1o  48568  itschlc0yqe  48610