Theorem 3imtr4d 297

Description: More general version of 3imtr4i 295. 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 262	. 2 ⊢ (𝜑 → (𝜓 → 𝜏))
5	1, 4	sylbid 243	1 ⊢ (𝜑 → (𝜃 → 𝜏))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  rmosn  4680  unielrel  6275  predtrss  6324  fvrnressn  7163  fconst5  7210  soisores  7333  caofrss  7730  caoftrn  7732  f1o2ndf1  8131  oaord  8548  omord2  8568  omcan  8570  oeord  8590  oecan  8591  nnaord  8621  nnmord  8634  omsmo  8660  pmss12g  8890  cantnf  9687  pm54.43  10075  ttukeylem2  10581  axlttrn  11375  axltadd  11376  axmulgt0  11377  axsup  11378  ltadd2  11407  ltord1  11835  recex  11941  ltmul1  12160  lt2msq  12195  nnge1  12359  zltp1le  12739  uzss  12981  eluzp1m1  12984  prodge0rd  13222  ixxssixx  13483  zesq  14363  pfxccatin12lem3  14874  swrdccat3blem  14881  relexpsucnnr  15171  climrlim2  15707  rlimres  15718  climshftlem  15734  lo1add  15787  lo1mul  15788  rlimsqzlem  15809  lo1le  15812  isercolllem2  15826  isercoll  15828  climsup  15830  cvgcmp  15976  climcndslem1  16011  dvds1lem  16430  sumodd  16551  rprpwr  16726  algcvg  16744  eucalgcvga  16754  rpexp12i  16893  crth  16948  pc2dvds  17050  pcmpt  17063  prmpwdvds  17075  1arith  17098  vdwlem2  17153  vdwlem6  17157  vdwlem8  17159  ercpbl  17714  initoid  18169  termoid  18170  ipopos  18703  insubm  19007  subginv  19336  symggrp  19607  f1otrspeq  19654  lsmless1x  19851  lsmless2x  19852  dprdss  20238  rngpropd  20389  dvdsunit  20602  irredrmul  20650  isdrngd  21015  isdrngdOLD  21017  lspextmo  21324  rngqiprngimf1lem  21583  domnchr  21831  zntoslem  21855  evlseu  22385  mat2pmatf1  23040  tgss  23279  neips  23424  opnnei  23431  lpss3  23455  ssrest  23487  t1t0  23659  kgen2ss  23867  isfild  24170  fgss  24185  fgss2  24186  cnpflf2  24312  fclsss1  24334  fclsss2  24335  tgpt0  24431  tsmsxp  24467  prdsxmslem2  24841  ngptgp  24948  nghmcn  25057  qdensere  25081  evth  25273  nmhmcn  25434  tcphcph  25551  caussi  25611  equivcfil  25613  rrxmvallem  25718  ivthlem2  25766  ovollb2lem  25802  ovolunlem1  25811  volun  25859  ioombl1lem4  25875  volsup2  25919  volcn  25920  ismbf3d  25968  itg2mulclem  26060  cpnord  26248  lhop1  26327  aaliou3lem2  26663  ulmclm  26707  ulmss  26717  abelth  26761  cosord  26852  efif1olem4  26866  argimgt0  26933  logdivlt  26942  cxploglim  27298  dvdssqf  27458  mumullem1  27499  mumullem2  27500  bposlem6  27609  lgsdchr  27675  gausslemma2dlem1a  27685  m1lgs  27708  chtppilim  27795  lestr  28112  lestric  28118  madebdayim  28267  madebdaylemold  28277  ltslpss  28287  om2noseqf1o  28680  zsoring  28788  bdaypw2n0bndlem  28842  bdayfin  28866  ax5seg  29509  axpasch  29512  axlowdimlem16  29528  axeuclid  29534  axcontlem4  29538  usgr1v0e  29900  nb3gr2nb  29958  cplgr1v  30004  finsumvtxdg2size  30124  usgr2pthlem  30342  clwwlknwwlksn  30622  erclwwlknsym  30654  erclwwlkntr  30655  frgr3vlem1  30867  3vfriswmgrlem  30871  numclwwlk5  30982  minvecolem5  31476  ocsh  31878  shless  31954  leopadd  32727  leopmuli  32728  leopmul2i  32730  leoptr  32732  spansncv2  32888  mdsl0  32905  ssdmd1  32908  cvdmd  32932  cdj3i  33036  uzssico  33369  expgt0b  33401  eqgvscpbl  33904  qusvscpbl  33905  cmpcref  34475  acycgrsubgr  35902  cvmliftmolem1  36025  satffunlem2lem2  36150  mrsubff1  36258  msubff1  36300  lediv2aALT  36421  cgr3tr4  36797  colinearxfr  36820  lineext  36821  brsegle  36853  seglecgr12im  36855  segletr  36859  colinbtwnle  36863  outsideoftr  36874  lineelsb2  36893  ltnmul  36945  ltnadd  36947  ivthALT  37103  tailfb  37145  poimirlem29  38547  itg2addnclem  38569  itg2addnclem3  38571  itg2addnc  38572  incsequz  38662  mettrifi  38671  ismtycnv  38716  bfplem1  38736  ghomco  38805  rngoisocnv  38895  keridl  38946  dmncan1  38990  ax12indalem  39982  ax12inda2ALT  39983  omllaw4  40283  cmtcomlemN  40285  cvlexch2  40366  cvlatexch2  40374  cvrexch  40457  atexchltN  40478  3atlem5  40524  lplnribN  40588  linepsubN  40789  paddss1  40854  paddss2  40855  pmapjoin  40889  pmapjat1  40890  cdleme36a  41497  dib2dim  42280  dih2dimbALTN  42282  djhcvat42  42452  dihjatcclem4  42458  dihjat1lem  42465  lcfrlem6  42584  hlhillcs  42995  oexpreposd  43359  mulgt0b1d  43516  mullt0b1d  43527  pell1234qrmulcl  43841  pell14qrss1234  43842  pell14qrmulcl  43849  pell14qrreccl  43850  pell1qrss14  43854  monotoddzzfi  43928  oddcomabszz  43930  omabs2  44318  omcl3g  44320  tfsconcat0b  44332  naddwordnexlem4  44387  climinf  46587  2ffzoeq  48367  iccpartgt  48478  pgnbgreunbgrlem1  49180  pgnbgreunbgrlem4  49186  upwlkwlk  49206  uspgrsprf1  49214  idomcanl  49413  rrx2xpref1o  49799  itschlc0yqe  49841  resipos  50052