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  4700  unielrel  6268  predtrss  6316  fvrnressn  7156  fconst5  7203  soisores  7325  caofrss  7715  caoftrn  7717  f1o2ndf1  8126  oaord  8564  omord2  8584  omcan  8586  oeord  8605  oecan  8606  nnaord  8636  nnmord  8649  omsmo  8675  pmss12g  8888  cantnf  9712  pm54.43  10020  ttukeylem2  10529  axlttrn  11312  axltadd  11313  axmulgt0  11314  axsup  11315  ltadd2  11344  ltord1  11768  recex  11874  ltmul1  12096  lt2msq  12132  nnge1  12273  zltp1le  12647  uzss  12880  eluzp1m1  12883  prodge0rd  13121  ixxssixx  13381  zesq  14249  pfxccatin12lem3  14755  swrdccat3blem  14762  relexpsucnnr  15049  climrlim2  15568  rlimres  15579  climshftlem  15595  lo1add  15648  lo1mul  15649  rlimsqzlem  15670  lo1le  15673  isercolllem2  15687  isercoll  15689  climsup  15691  cvgcmp  15837  climcndslem1  15870  dvds1lem  16292  sumodd  16412  rprpwr  16583  algcvg  16600  eucalgcvga  16610  rpexp12i  16748  crth  16802  pc2dvds  16904  pcmpt  16917  prmpwdvds  16929  1arith  16952  vdwlem2  17007  vdwlem6  17011  vdwlem8  17013  ercpbl  17568  initoid  18019  termoid  18020  ipopos  18551  insubm  18801  subginv  19121  symggrp  19386  f1otrspeq  19433  lsmless1x  19630  lsmless2x  19631  dprdss  20017  rngpropd  20139  dvdsunit  20344  irredrmul  20392  isdrngd  20730  isdrngdOLD  20732  lspextmo  21019  rngqiprngimf1lem  21260  domnchr  21498  zntoslem  21522  evlseu  22046  mat2pmatf1  22672  tgss  22911  neips  23056  opnnei  23063  lpss3  23087  ssrest  23119  t1t0  23291  kgen2ss  23498  isfild  23801  fgss  23816  fgss2  23817  cnpflf2  23943  fclsss1  23965  fclsss2  23966  tgpt0  24062  tsmsxp  24098  prdsxmslem2  24473  ngptgp  24580  nghmcn  24689  qdensere  24713  evth  24914  nmhmcn  25076  tcphcph  25194  caussi  25254  equivcfil  25256  rrxmvallem  25361  ivthlem2  25410  ovollb2lem  25446  ovolunlem1  25455  volun  25503  ioombl1lem4  25519  volsup2  25563  volcn  25564  ismbf3d  25612  itg2mulclem  25704  cpnord  25894  lhop1  25976  aaliou3lem2  26308  ulmclm  26353  ulmss  26363  abelth  26408  cosord  26497  efif1olem4  26511  argimgt0  26578  logdivlt  26587  cxploglim  26945  dvdssqf  27105  mumullem1  27146  mumullem2  27147  bposlem6  27257  lgsdchr  27323  gausslemma2dlem1a  27333  m1lgs  27356  chtppilim  27443  sletr  27727  sletric  27733  madebdayim  27856  madebdaylemold  27866  sltlpss  27876  om2noseqf1o  28252  ax5seg  28922  axpasch  28925  axlowdimlem16  28941  axeuclid  28947  axcontlem4  28951  usgr1v0e  29310  nb3gr2nb  29368  cplgr1v  29414  finsumvtxdg2size  29535  usgr2pthlem  29750  clwwlknwwlksn  30024  erclwwlknsym  30056  erclwwlkntr  30057  frgr3vlem1  30259  3vfriswmgrlem  30263  numclwwlk5  30374  minvecolem5  30867  ocsh  31269  shless  31345  leopadd  32118  leopmuli  32119  leopmul2i  32121  leoptr  32123  spansncv2  32279  mdsl0  32296  ssdmd1  32299  cvdmd  32323  cdj3i  32427  uzssico  32766  expgt0b  32800  eqgvscpbl  33370  qusvscpbl  33371  cmpcref  33886  acycgrsubgr  35185  cvmliftmolem1  35308  satffunlem2lem2  35433  mrsubff1  35541  msubff1  35583  lediv2aALT  35704  cgr3tr4  36075  colinearxfr  36098  lineext  36099  brsegle  36131  seglecgr12im  36133  segletr  36137  colinbtwnle  36141  outsideoftr  36152  lineelsb2  36171  ivthALT  36358  tailfb  36400  poimirlem29  37678  itg2addnclem  37700  itg2addnclem3  37702  itg2addnc  37703  incsequz  37777  mettrifi  37786  ismtycnv  37831  bfplem1  37851  ghomco  37920  rngoisocnv  38010  keridl  38061  dmncan1  38105  ax12indalem  38968  ax12inda2ALT  38969  omllaw4  39269  cmtcomlemN  39271  cvlexch2  39352  cvlatexch2  39360  cvrexch  39444  atexchltN  39465  3atlem5  39511  lplnribN  39575  linepsubN  39776  paddss1  39841  paddss2  39842  pmapjoin  39876  pmapjat1  39877  cdleme36a  40484  dib2dim  41267  dih2dimbALTN  41269  djhcvat42  41439  dihjatcclem4  41445  dihjat1lem  41452  lcfrlem6  41571  hlhillcs  41982  oexpreposd  42340  mulgt0b2d  42478  pell1234qrmulcl  42853  pell14qrss1234  42854  pell14qrmulcl  42861  pell14qrreccl  42862  pell1qrss14  42866  monotoddzzfi  42941  oddcomabszz  42943  omabs2  43331  omcl3g  43333  tfsconcat0b  43345  naddwordnexlem4  43400  climinf  45615  2ffzoeq  47336  iccpartgt  47421  upwlkwlk  48094  uspgrsprf1  48102  rrx2xpref1o  48678  itschlc0yqe  48720  resipos  48929