Theorem 3imtr4d 293

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

Syntax hints:   → wi 4   ↔ wb 205

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 206

This theorem is referenced by:  rmosn  4685  unielrel  6231  predtrss  6281  fvrnressn  7112  fconst5  7160  soisores  7277  caofrss  7658  caoftrn  7660  f1o2ndf1  8059  oaord  8499  omord2  8519  omcan  8521  oeord  8540  oecan  8541  nnaord  8571  nnmord  8584  omsmo  8609  pmss12g  8814  cantnf  9638  pm54.43  9946  ttukeylem2  10455  axlttrn  11236  axltadd  11237  axmulgt0  11238  axsup  11239  ltadd2  11268  ltord1  11690  recex  11796  ltmul1  12014  lt2msq  12049  nnge1  12190  zltp1le  12562  uzss  12795  eluzp1m1  12798  prodge0rd  13031  ixxssixx  13288  zesq  14139  pfxccatin12lem3  14632  swrdccat3blem  14639  relexpsucnnr  14922  climrlim2  15441  rlimres  15452  climshftlem  15468  lo1add  15521  lo1mul  15522  rlimsqzlem  15545  lo1le  15548  isercolllem2  15562  isercoll  15564  climsup  15566  cvgcmp  15712  climcndslem1  15745  dvds1lem  16161  sumodd  16281  rprpwr  16450  algcvg  16463  eucalgcvga  16473  rpexp12i  16611  crth  16661  pc2dvds  16762  pcmpt  16775  prmpwdvds  16787  1arith  16810  vdwlem2  16865  vdwlem6  16869  vdwlem8  16871  ercpbl  17445  initoid  17901  termoid  17902  ipopos  18439  insubm  18643  subginv  18949  symggrp  19196  f1otrspeq  19243  lsmless1x  19440  lsmless2x  19441  dprdss  19822  dvdsunit  20106  irredrmul  20152  isdrngd  20255  isdrngdOLD  20257  lspextmo  20574  domnchr  20972  zntoslem  21000  evlseu  21530  mat2pmatf1  22115  tgss  22355  neips  22501  opnnei  22508  lpss3  22532  ssrest  22564  t1t0  22736  kgen2ss  22943  isfild  23246  fgss  23261  fgss2  23262  cnpflf2  23388  fclsss1  23410  fclsss2  23411  tgpt0  23507  tsmsxp  23543  prdsxmslem2  23922  ngptgp  24029  nghmcn  24146  qdensere  24170  evth  24359  nmhmcn  24520  tcphcph  24638  caussi  24698  equivcfil  24700  rrxmvallem  24805  ivthlem2  24853  ovollb2lem  24889  ovolunlem1  24898  volun  24946  ioombl1lem4  24962  volsup2  25006  volcn  25007  ismbf3d  25055  itg2mulclem  25148  cpnord  25336  lhop1  25415  aaliou3lem2  25740  ulmclm  25783  ulmss  25793  abelth  25837  cosord  25924  efif1olem4  25938  argimgt0  26004  logdivlt  26013  cxploglim  26364  dvdssqf  26524  mumullem1  26565  mumullem2  26566  bposlem6  26674  lgsdchr  26740  gausslemma2dlem1a  26750  m1lgs  26773  chtppilim  26860  sletr  27143  sletric  27149  madebdayim  27260  madebdaylemold  27270  sltlpss  27279  ax5seg  27950  axpasch  27953  axlowdimlem16  27969  axeuclid  27975  axcontlem4  27979  usgr1v0e  28337  nb3gr2nb  28395  cplgr1v  28441  finsumvtxdg2size  28561  usgr2pthlem  28774  clwwlknwwlksn  29045  erclwwlknsym  29077  erclwwlkntr  29078  frgr3vlem1  29280  3vfriswmgrlem  29284  numclwwlk5  29395  minvecolem5  29886  ocsh  30288  shless  30364  leopadd  31137  leopmuli  31138  leopmul2i  31140  leoptr  31142  spansncv2  31298  mdsl0  31315  ssdmd1  31318  cvdmd  31342  cdj3i  31446  uzssico  31755  eqgvscpbl  32213  qusvscpbl  32214  cmpcref  32520  acycgrsubgr  33839  cvmliftmolem1  33962  satffunlem2lem2  34087  mrsubff1  34195  msubff1  34237  lediv2aALT  34352  cgr3tr4  34713  colinearxfr  34736  lineext  34737  brsegle  34769  seglecgr12im  34771  segletr  34775  colinbtwnle  34779  outsideoftr  34790  lineelsb2  34809  ivthALT  34883  tailfb  34925  poimirlem29  36180  itg2addnclem  36202  itg2addnclem3  36204  itg2addnc  36205  incsequz  36280  mettrifi  36289  ismtycnv  36334  bfplem1  36354  ghomco  36423  rngoisocnv  36513  keridl  36564  dmncan1  36608  ax12indalem  37480  ax12inda2ALT  37481  omllaw4  37781  cmtcomlemN  37783  cvlexch2  37864  cvlatexch2  37872  cvrexch  37956  atexchltN  37977  3atlem5  38023  lplnribN  38087  linepsubN  38288  paddss1  38353  paddss2  38354  pmapjoin  38388  pmapjat1  38389  cdleme36a  38996  dib2dim  39779  dih2dimbALTN  39781  djhcvat42  39951  dihjatcclem4  39957  dihjat1lem  39964  lcfrlem6  40083  hlhillcs  40498  oexpreposd  40865  mulgt0b2d  40987  pell1234qrmulcl  41236  pell14qrss1234  41237  pell14qrmulcl  41244  pell14qrreccl  41245  pell1qrss14  41249  monotoddzzfi  41324  oddcomabszz  41326  omabs2  41725  omcl3g  41727  tfsconcat0b  41739  naddwordnexlem4  41795  climinf  43967  2ffzoeq  45680  iccpartgt  45739  upwlkwlk  46161  uspgrsprf1  46169  rrx2xpref1o  46924  itschlc0yqe  46966