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  4652  unielrel  6166  predtrss  6214  fvrnressn  7015  fconst5  7063  soisores  7178  caofrss  7547  caoftrn  7549  f1o2ndf1  7934  oaord  8340  omord2  8360  omcan  8362  oeord  8381  oecan  8382  nnaord  8412  nnmord  8425  omsmo  8448  pmss12g  8615  cantnf  9381  pm54.43  9690  ttukeylem2  10197  axlttrn  10978  axltadd  10979  axmulgt0  10980  axsup  10981  ltadd2  11009  ltord1  11431  recex  11537  ltmul1  11755  lt2msq  11790  nnge1  11931  zltp1le  12300  uzss  12534  eluzp1m1  12537  prodge0rd  12766  ixxssixx  13022  zesq  13869  pfxccatin12lem3  14373  swrdccat3blem  14380  relexpsucnnr  14664  climrlim2  15184  rlimres  15195  climshftlem  15211  lo1add  15264  lo1mul  15265  rlimsqzlem  15288  lo1le  15291  isercolllem2  15305  isercoll  15307  climsup  15309  cvgcmp  15456  climcndslem1  15489  dvds1lem  15905  sumodd  16025  rprpwr  16196  algcvg  16209  eucalgcvga  16219  rpexp12i  16357  crth  16407  pc2dvds  16508  pcmpt  16521  prmpwdvds  16533  1arith  16556  vdwlem2  16611  vdwlem6  16615  vdwlem8  16617  ercpbl  17177  initoid  17632  termoid  17633  ipopos  18169  insubm  18372  subginv  18677  symggrp  18923  f1otrspeq  18970  lsmless1x  19164  lsmless2x  19165  dprdss  19547  dvdsunit  19820  irredrmul  19864  isdrngd  19931  lspextmo  20233  domnchr  20648  zntoslem  20676  evlseu  21203  mat2pmatf1  21786  tgss  22026  neips  22172  opnnei  22179  lpss3  22203  ssrest  22235  t1t0  22407  kgen2ss  22614  isfild  22917  fgss  22932  fgss2  22933  cnpflf2  23059  fclsss1  23081  fclsss2  23082  tgpt0  23178  tsmsxp  23214  prdsxmslem2  23591  ngptgp  23698  nghmcn  23815  qdensere  23839  evth  24028  nmhmcn  24189  tcphcph  24306  caussi  24366  equivcfil  24368  rrxmvallem  24473  ivthlem2  24521  ovollb2lem  24557  ovolunlem1  24566  volun  24614  ioombl1lem4  24630  volsup2  24674  volcn  24675  ismbf3d  24723  itg2mulclem  24816  cpnord  25004  lhop1  25083  aaliou3lem2  25408  ulmclm  25451  ulmss  25461  abelth  25505  cosord  25592  efif1olem4  25606  argimgt0  25672  logdivlt  25681  cxploglim  26032  dvdssqf  26192  mumullem1  26233  mumullem2  26234  bposlem6  26342  lgsdchr  26408  gausslemma2dlem1a  26418  m1lgs  26441  chtppilim  26528  ax5seg  27209  axpasch  27212  axlowdimlem16  27228  axeuclid  27234  axcontlem4  27238  usgr1v0e  27596  nb3gr2nb  27654  cplgr1v  27700  finsumvtxdg2size  27820  usgr2pthlem  28032  clwwlknwwlksn  28303  erclwwlknsym  28335  erclwwlkntr  28336  frgr3vlem1  28538  3vfriswmgrlem  28542  numclwwlk5  28653  minvecolem5  29144  ocsh  29546  shless  29622  leopadd  30395  leopmuli  30396  leopmul2i  30398  leoptr  30400  spansncv2  30556  mdsl0  30573  ssdmd1  30576  cvdmd  30600  cdj3i  30704  uzssico  31007  eqgvscpbl  31452  qusvscpbl  31453  cmpcref  31702  acycgrsubgr  33020  cvmliftmolem1  33143  satffunlem2lem2  33268  mrsubff1  33376  msubff1  33418  lediv2aALT  33535  sletr  33888  madebdayim  33997  madebdaylemold  34005  sltlpss  34014  cgr3tr4  34281  colinearxfr  34304  lineext  34305  brsegle  34337  seglecgr12im  34339  segletr  34343  colinbtwnle  34347  outsideoftr  34358  lineelsb2  34377  ivthALT  34451  tailfb  34493  poimirlem29  35733  itg2addnclem  35755  itg2addnclem3  35757  itg2addnc  35758  incsequz  35833  mettrifi  35842  ismtycnv  35887  bfplem1  35907  ghomco  35976  rngoisocnv  36066  keridl  36117  dmncan1  36161  ax12indalem  36886  ax12inda2ALT  36887  omllaw4  37187  cmtcomlemN  37189  cvlexch2  37270  cvlatexch2  37278  cvrexch  37361  atexchltN  37382  3atlem5  37428  lplnribN  37492  linepsubN  37693  paddss1  37758  paddss2  37759  pmapjoin  37793  pmapjat1  37794  cdleme36a  38401  dib2dim  39184  dih2dimbALTN  39186  djhcvat42  39356  dihjatcclem4  39362  dihjat1lem  39369  lcfrlem6  39488  hlhillcs  39903  oexpreposd  40242  mulgt0b2d  40351  pell1234qrmulcl  40593  pell14qrss1234  40594  pell14qrmulcl  40601  pell14qrreccl  40602  pell1qrss14  40606  monotoddzzfi  40680  oddcomabszz  40682  climinf  43037  2ffzoeq  44708  iccpartgt  44767  upwlkwlk  45189  uspgrsprf1  45197  rrx2xpref1o  45952  itschlc0yqe  45994