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  4744  unielrel  6305  predtrss  6354  fvrnressn  7195  fconst5  7243  soisores  7363  caofrss  7751  caoftrn  7753  f1o2ndf1  8163  oaord  8603  omord2  8623  omcan  8625  oeord  8644  oecan  8645  nnaord  8675  nnmord  8688  omsmo  8714  pmss12g  8927  cantnf  9762  pm54.43  10070  ttukeylem2  10579  axlttrn  11362  axltadd  11363  axmulgt0  11364  axsup  11365  ltadd2  11394  ltord1  11816  recex  11922  ltmul1  12144  lt2msq  12180  nnge1  12321  zltp1le  12693  uzss  12926  eluzp1m1  12929  prodge0rd  13164  ixxssixx  13421  zesq  14275  pfxccatin12lem3  14780  swrdccat3blem  14787  relexpsucnnr  15074  climrlim2  15593  rlimres  15604  climshftlem  15620  lo1add  15673  lo1mul  15674  rlimsqzlem  15697  lo1le  15700  isercolllem2  15714  isercoll  15716  climsup  15718  cvgcmp  15864  climcndslem1  15897  dvds1lem  16316  sumodd  16436  rprpwr  16606  algcvg  16623  eucalgcvga  16633  rpexp12i  16771  crth  16825  pc2dvds  16926  pcmpt  16939  prmpwdvds  16951  1arith  16974  vdwlem2  17029  vdwlem6  17033  vdwlem8  17035  ercpbl  17609  initoid  18068  termoid  18069  ipopos  18606  insubm  18853  subginv  19173  symggrp  19442  f1otrspeq  19489  lsmless1x  19686  lsmless2x  19687  dprdss  20073  rngpropd  20201  dvdsunit  20405  irredrmul  20453  isdrngd  20787  isdrngdOLD  20789  lspextmo  21078  rngqiprngimf1lem  21327  domnchr  21570  zntoslem  21598  evlseu  22130  mat2pmatf1  22756  tgss  22996  neips  23142  opnnei  23149  lpss3  23173  ssrest  23205  t1t0  23377  kgen2ss  23584  isfild  23887  fgss  23902  fgss2  23903  cnpflf2  24029  fclsss1  24051  fclsss2  24052  tgpt0  24148  tsmsxp  24184  prdsxmslem2  24563  ngptgp  24670  nghmcn  24787  qdensere  24811  evth  25010  nmhmcn  25172  tcphcph  25290  caussi  25350  equivcfil  25352  rrxmvallem  25457  ivthlem2  25506  ovollb2lem  25542  ovolunlem1  25551  volun  25599  ioombl1lem4  25615  volsup2  25659  volcn  25660  ismbf3d  25708  itg2mulclem  25801  cpnord  25991  lhop1  26073  aaliou3lem2  26403  ulmclm  26448  ulmss  26458  abelth  26503  cosord  26591  efif1olem4  26605  argimgt0  26672  logdivlt  26681  cxploglim  27039  dvdssqf  27199  mumullem1  27240  mumullem2  27241  bposlem6  27351  lgsdchr  27417  gausslemma2dlem1a  27427  m1lgs  27450  chtppilim  27537  sletr  27821  sletric  27827  madebdayim  27944  madebdaylemold  27954  sltlpss  27963  om2noseqf1o  28325  ax5seg  28971  axpasch  28974  axlowdimlem16  28990  axeuclid  28996  axcontlem4  29000  usgr1v0e  29361  nb3gr2nb  29419  cplgr1v  29465  finsumvtxdg2size  29586  usgr2pthlem  29799  clwwlknwwlksn  30070  erclwwlknsym  30102  erclwwlkntr  30103  frgr3vlem1  30305  3vfriswmgrlem  30309  numclwwlk5  30420  minvecolem5  30913  ocsh  31315  shless  31391  leopadd  32164  leopmuli  32165  leopmul2i  32167  leoptr  32169  spansncv2  32325  mdsl0  32342  ssdmd1  32345  cvdmd  32369  cdj3i  32473  uzssico  32789  expgt0b  32820  eqgvscpbl  33343  qusvscpbl  33344  cmpcref  33796  acycgrsubgr  35126  cvmliftmolem1  35249  satffunlem2lem2  35374  mrsubff1  35482  msubff1  35524  lediv2aALT  35645  cgr3tr4  36016  colinearxfr  36039  lineext  36040  brsegle  36072  seglecgr12im  36074  segletr  36078  colinbtwnle  36082  outsideoftr  36093  lineelsb2  36112  ivthALT  36301  tailfb  36343  poimirlem29  37609  itg2addnclem  37631  itg2addnclem3  37633  itg2addnc  37634  incsequz  37708  mettrifi  37717  ismtycnv  37762  bfplem1  37782  ghomco  37851  rngoisocnv  37941  keridl  37992  dmncan1  38036  ax12indalem  38901  ax12inda2ALT  38902  omllaw4  39202  cmtcomlemN  39204  cvlexch2  39285  cvlatexch2  39293  cvrexch  39377  atexchltN  39398  3atlem5  39444  lplnribN  39508  linepsubN  39709  paddss1  39774  paddss2  39775  pmapjoin  39809  pmapjat1  39810  cdleme36a  40417  dib2dim  41200  dih2dimbALTN  41202  djhcvat42  41372  dihjatcclem4  41378  dihjat1lem  41385  lcfrlem6  41504  hlhillcs  41919  oexpreposd  42309  mulgt0b2d  42436  pell1234qrmulcl  42811  pell14qrss1234  42812  pell14qrmulcl  42819  pell14qrreccl  42820  pell1qrss14  42824  monotoddzzfi  42899  oddcomabszz  42901  omabs2  43294  omcl3g  43296  tfsconcat0b  43308  naddwordnexlem4  43363  climinf  45527  2ffzoeq  47242  iccpartgt  47301  upwlkwlk  47862  uspgrsprf1  47870  rrx2xpref1o  48452  itschlc0yqe  48494