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  4664  unielrel  6230  predtrss  6278  fvrnressn  7106  fconst5  7152  soisores  7273  caofrss  7661  caoftrn  7663  f1o2ndf1  8063  oaord  8473  omord2  8493  omcan  8495  oeord  8515  oecan  8516  nnaord  8546  nnmord  8559  omsmo  8585  pmss12g  8808  cantnf  9603  pm54.43  9914  ttukeylem2  10421  axlttrn  11207  axltadd  11208  axmulgt0  11209  axsup  11210  ltadd2  11239  ltord1  11665  recex  11771  ltmul1  11994  lt2msq  12030  nnge1  12194  zltp1le  12566  uzss  12800  eluzp1m1  12803  prodge0rd  13040  ixxssixx  13301  zesq  14177  pfxccatin12lem3  14683  swrdccat3blem  14690  relexpsucnnr  14976  climrlim2  15498  rlimres  15509  climshftlem  15525  lo1add  15578  lo1mul  15579  rlimsqzlem  15600  lo1le  15603  isercolllem2  15617  isercoll  15619  climsup  15621  cvgcmp  15768  climcndslem1  15803  dvds1lem  16225  sumodd  16346  rprpwr  16517  algcvg  16534  eucalgcvga  16544  rpexp12i  16683  crth  16737  pc2dvds  16839  pcmpt  16852  prmpwdvds  16864  1arith  16887  vdwlem2  16942  vdwlem6  16946  vdwlem8  16948  ercpbl  17502  initoid  17957  termoid  17958  ipopos  18491  insubm  18775  subginv  19098  symggrp  19364  f1otrspeq  19411  lsmless1x  19608  lsmless2x  19609  dprdss  19995  rngpropd  20144  dvdsunit  20348  irredrmul  20396  isdrngd  20731  isdrngdOLD  20733  lspextmo  21041  rngqiprngimf1lem  21282  domnchr  21520  zntoslem  21544  evlseu  22070  mat2pmatf1  22703  tgss  22942  neips  23087  opnnei  23094  lpss3  23118  ssrest  23150  t1t0  23322  kgen2ss  23529  isfild  23832  fgss  23847  fgss2  23848  cnpflf2  23974  fclsss1  23996  fclsss2  23997  tgpt0  24093  tsmsxp  24129  prdsxmslem2  24503  ngptgp  24610  nghmcn  24719  qdensere  24743  evth  24935  nmhmcn  25096  tcphcph  25213  caussi  25273  equivcfil  25275  rrxmvallem  25380  ivthlem2  25428  ovollb2lem  25464  ovolunlem1  25473  volun  25521  ioombl1lem4  25537  volsup2  25581  volcn  25582  ismbf3d  25630  itg2mulclem  25722  cpnord  25911  lhop1  25991  aaliou3lem2  26322  ulmclm  26367  ulmss  26377  abelth  26422  cosord  26511  efif1olem4  26525  argimgt0  26592  logdivlt  26601  cxploglim  26959  dvdssqf  27119  mumullem1  27160  mumullem2  27161  bposlem6  27271  lgsdchr  27337  gausslemma2dlem1a  27347  m1lgs  27370  chtppilim  27457  lestr  27745  lestric  27751  madebdayim  27899  madebdaylemold  27909  ltslpss  27919  om2noseqf1o  28312  zsoring  28420  bdaypw2n0bndlem  28474  bdayfin  28498  ax5seg  29026  axpasch  29029  axlowdimlem16  29045  axeuclid  29051  axcontlem4  29055  usgr1v0e  29414  nb3gr2nb  29472  cplgr1v  29518  finsumvtxdg2size  29639  usgr2pthlem  29851  clwwlknwwlksn  30128  erclwwlknsym  30160  erclwwlkntr  30161  frgr3vlem1  30363  3vfriswmgrlem  30367  numclwwlk5  30478  minvecolem5  30972  ocsh  31374  shless  31450  leopadd  32223  leopmuli  32224  leopmul2i  32226  leoptr  32228  spansncv2  32384  mdsl0  32401  ssdmd1  32404  cvdmd  32428  cdj3i  32532  uzssico  32877  expgt0b  32910  eqgvscpbl  33430  qusvscpbl  33431  cmpcref  34015  acycgrsubgr  35361  cvmliftmolem1  35484  satffunlem2lem2  35609  mrsubff1  35717  msubff1  35759  lediv2aALT  35880  cgr3tr4  36255  colinearxfr  36278  lineext  36279  brsegle  36311  seglecgr12im  36313  segletr  36317  colinbtwnle  36321  outsideoftr  36332  lineelsb2  36351  ivthALT  36538  tailfb  36580  poimirlem29  37981  itg2addnclem  38003  itg2addnclem3  38005  itg2addnc  38006  incsequz  38080  mettrifi  38089  ismtycnv  38134  bfplem1  38154  ghomco  38223  rngoisocnv  38313  keridl  38364  dmncan1  38408  ax12indalem  39402  ax12inda2ALT  39403  omllaw4  39703  cmtcomlemN  39705  cvlexch2  39786  cvlatexch2  39794  cvrexch  39877  atexchltN  39898  3atlem5  39944  lplnribN  40008  linepsubN  40209  paddss1  40274  paddss2  40275  pmapjoin  40309  pmapjat1  40310  cdleme36a  40917  dib2dim  41700  dih2dimbALTN  41702  djhcvat42  41872  dihjatcclem4  41878  dihjat1lem  41885  lcfrlem6  42004  hlhillcs  42415  oexpreposd  42765  mulgt0b1d  42928  mullt0b1d  42939  pell1234qrmulcl  43298  pell14qrss1234  43299  pell14qrmulcl  43306  pell14qrreccl  43307  pell1qrss14  43311  monotoddzzfi  43385  oddcomabszz  43387  omabs2  43775  omcl3g  43777  tfsconcat0b  43789  naddwordnexlem4  43844  climinf  46051  2ffzoeq  47773  iccpartgt  47884  pgnbgreunbgrlem1  48586  pgnbgreunbgrlem4  48592  upwlkwlk  48612  uspgrsprf1  48620  rrx2xpref1o  49191  itschlc0yqe  49233  resipos  49447