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 ⊢ (𝜑 → (𝜃 → 𝜏))

Syntax hints:   → wi 4   ↔ wb 209

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 210

This theorem is referenced by:  rmosn  4685  unielrel  6275  predtrss  6323  fvrnressn  7158  fconst5  7204  soisores  7325  caofrss  7713  caoftrn  7715  f1o2ndf1  8113  oaord  8528  omord2  8548  omcan  8550  oeord  8570  oecan  8571  nnaord  8601  nnmord  8614  omsmo  8640  pmss12g  8863  cantnf  9658  pm54.43  9983  ttukeylem2  10489  axlttrn  11277  axltadd  11278  axmulgt0  11279  axsup  11280  ltadd2  11309  ltord1  11735  recex  11841  ltmul1  12060  lt2msq  12095  nnge1  12259  zltp1le  12639  uzss  12880  eluzp1m1  12883  prodge0rd  13120  ixxssixx  13381  zesq  14258  pfxccatin12lem3  14765  swrdccat3blem  14772  relexpsucnnr  15058  climrlim2  15594  rlimres  15605  climshftlem  15621  lo1add  15674  lo1mul  15675  rlimsqzlem  15696  lo1le  15699  isercolllem2  15713  isercoll  15715  climsup  15717  cvgcmp  15864  climcndslem1  15899  dvds1lem  16320  sumodd  16441  rprpwr  16612  algcvg  16629  eucalgcvga  16639  rpexp12i  16778  crth  16832  pc2dvds  16934  pcmpt  16947  prmpwdvds  16959  1arith  16982  vdwlem2  17037  vdwlem6  17041  vdwlem8  17043  ercpbl  17598  initoid  18053  termoid  18054  ipopos  18587  insubm  18872  subginv  19194  symggrp  19465  f1otrspeq  19512  lsmless1x  19709  lsmless2x  19710  dprdss  20096  rngpropd  20247  dvdsunit  20457  irredrmul  20505  isdrngd  20868  isdrngdOLD  20870  lspextmo  21177  rngqiprngimf1lem  21434  domnchr  21682  zntoslem  21706  evlseu  22234  mat2pmatf1  22886  tgss  23125  neips  23270  opnnei  23277  lpss3  23301  ssrest  23333  t1t0  23505  kgen2ss  23712  isfild  24015  fgss  24030  fgss2  24031  cnpflf2  24157  fclsss1  24179  fclsss2  24180  tgpt0  24276  tsmsxp  24312  prdsxmslem2  24686  ngptgp  24793  nghmcn  24902  qdensere  24926  evth  25118  nmhmcn  25279  tcphcph  25396  caussi  25456  equivcfil  25458  rrxmvallem  25563  ivthlem2  25611  ovollb2lem  25647  ovolunlem1  25656  volun  25704  ioombl1lem4  25720  volsup2  25764  volcn  25765  ismbf3d  25813  itg2mulclem  25905  cpnord  26094  lhop1  26173  aaliou3lem2  26506  ulmclm  26550  ulmss  26560  abelth  26604  cosord  26696  efif1olem4  26710  argimgt0  26777  logdivlt  26786  cxploglim  27142  dvdssqf  27302  mumullem1  27343  mumullem2  27344  bposlem6  27453  lgsdchr  27519  gausslemma2dlem1a  27529  m1lgs  27552  chtppilim  27639  lestr  27926  lestric  27932  madebdayim  28081  madebdaylemold  28091  ltslpss  28101  om2noseqf1o  28494  zsoring  28602  bdaypw2n0bndlem  28656  bdayfin  28680  ax5seg  29288  axpasch  29291  axlowdimlem16  29307  axeuclid  29313  axcontlem4  29317  usgr1v0e  29676  nb3gr2nb  29734  cplgr1v  29780  finsumvtxdg2size  29900  usgr2pthlem  30112  clwwlknwwlksn  30389  erclwwlknsym  30421  erclwwlkntr  30422  frgr3vlem1  30624  3vfriswmgrlem  30628  numclwwlk5  30739  minvecolem5  31233  ocsh  31635  shless  31711  leopadd  32484  leopmuli  32485  leopmul2i  32487  leoptr  32489  spansncv2  32645  mdsl0  32662  ssdmd1  32665  cvdmd  32689  cdj3i  32793  uzssico  33129  expgt0b  33161  eqgvscpbl  33670  qusvscpbl  33671  cmpcref  34240  acycgrsubgr  35650  cvmliftmolem1  35773  satffunlem2lem2  35898  mrsubff1  36006  msubff1  36048  lediv2aALT  36169  cgr3tr4  36544  colinearxfr  36567  lineext  36568  brsegle  36600  seglecgr12im  36602  segletr  36606  colinbtwnle  36610  outsideoftr  36621  lineelsb2  36640  ltnmul  36693  ltnadd  36695  ivthALT  36846  tailfb  36888  poimirlem29  38300  itg2addnclem  38322  itg2addnclem3  38324  itg2addnc  38325  incsequz  38399  mettrifi  38408  ismtycnv  38453  bfplem1  38473  ghomco  38542  rngoisocnv  38632  keridl  38683  dmncan1  38727  ax12indalem  39719  ax12inda2ALT  39720  omllaw4  40020  cmtcomlemN  40022  cvlexch2  40103  cvlatexch2  40111  cvrexch  40194  atexchltN  40215  3atlem5  40261  lplnribN  40325  linepsubN  40526  paddss1  40591  paddss2  40592  pmapjoin  40626  pmapjat1  40627  cdleme36a  41234  dib2dim  42017  dih2dimbALTN  42019  djhcvat42  42189  dihjatcclem4  42195  dihjat1lem  42202  lcfrlem6  42321  hlhillcs  42732  oexpreposd  43083  mulgt0b1d  43246  mullt0b1d  43257  pell1234qrmulcl  43582  pell14qrss1234  43583  pell14qrmulcl  43590  pell14qrreccl  43591  pell1qrss14  43595  monotoddzzfi  43669  oddcomabszz  43671  omabs2  44059  omcl3g  44061  tfsconcat0b  44073  naddwordnexlem4  44128  climinf  46322  2ffzoeq  48065  iccpartgt  48176  pgnbgreunbgrlem1  48878  pgnbgreunbgrlem4  48884  upwlkwlk  48904  uspgrsprf1  48912  idomcanl  49112  rrx2xpref1o  49498  itschlc0yqe  49540  resipos  49753