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  4663  unielrel  6238  predtrss  6286  fvrnressn  7115  fconst5  7161  soisores  7282  caofrss  7670  caoftrn  7672  f1o2ndf1  8072  oaord  8482  omord2  8502  omcan  8504  oeord  8524  oecan  8525  nnaord  8555  nnmord  8568  omsmo  8594  pmss12g  8817  cantnf  9614  pm54.43  9925  ttukeylem2  10432  axlttrn  11218  axltadd  11219  axmulgt0  11220  axsup  11221  ltadd2  11250  ltord1  11676  recex  11782  ltmul1  12005  lt2msq  12041  nnge1  12205  zltp1le  12577  uzss  12811  eluzp1m1  12814  prodge0rd  13051  ixxssixx  13312  zesq  14188  pfxccatin12lem3  14694  swrdccat3blem  14701  relexpsucnnr  14987  climrlim2  15509  rlimres  15520  climshftlem  15536  lo1add  15589  lo1mul  15590  rlimsqzlem  15611  lo1le  15614  isercolllem2  15628  isercoll  15630  climsup  15632  cvgcmp  15779  climcndslem1  15814  dvds1lem  16236  sumodd  16357  rprpwr  16528  algcvg  16545  eucalgcvga  16555  rpexp12i  16694  crth  16748  pc2dvds  16850  pcmpt  16863  prmpwdvds  16875  1arith  16898  vdwlem2  16953  vdwlem6  16957  vdwlem8  16959  ercpbl  17513  initoid  17968  termoid  17969  ipopos  18502  insubm  18786  subginv  19109  symggrp  19375  f1otrspeq  19422  lsmless1x  19619  lsmless2x  19620  dprdss  20006  rngpropd  20155  dvdsunit  20359  irredrmul  20407  isdrngd  20742  isdrngdOLD  20744  lspextmo  21051  rngqiprngimf1lem  21292  domnchr  21512  zntoslem  21536  evlseu  22061  mat2pmatf1  22694  tgss  22933  neips  23078  opnnei  23085  lpss3  23109  ssrest  23141  t1t0  23313  kgen2ss  23520  isfild  23823  fgss  23838  fgss2  23839  cnpflf2  23965  fclsss1  23987  fclsss2  23988  tgpt0  24084  tsmsxp  24120  prdsxmslem2  24494  ngptgp  24601  nghmcn  24710  qdensere  24734  evth  24926  nmhmcn  25087  tcphcph  25204  caussi  25264  equivcfil  25266  rrxmvallem  25371  ivthlem2  25419  ovollb2lem  25455  ovolunlem1  25464  volun  25512  ioombl1lem4  25528  volsup2  25572  volcn  25573  ismbf3d  25621  itg2mulclem  25713  cpnord  25902  lhop1  25981  aaliou3lem2  26309  ulmclm  26352  ulmss  26362  abelth  26406  cosord  26495  efif1olem4  26509  argimgt0  26576  logdivlt  26585  cxploglim  26941  dvdssqf  27101  mumullem1  27142  mumullem2  27143  bposlem6  27252  lgsdchr  27318  gausslemma2dlem1a  27328  m1lgs  27351  chtppilim  27438  lestr  27726  lestric  27732  madebdayim  27880  madebdaylemold  27890  ltslpss  27900  om2noseqf1o  28293  zsoring  28401  bdaypw2n0bndlem  28455  bdayfin  28479  ax5seg  29007  axpasch  29010  axlowdimlem16  29026  axeuclid  29032  axcontlem4  29036  usgr1v0e  29395  nb3gr2nb  29453  cplgr1v  29499  finsumvtxdg2size  29619  usgr2pthlem  29831  clwwlknwwlksn  30108  erclwwlknsym  30140  erclwwlkntr  30141  frgr3vlem1  30343  3vfriswmgrlem  30347  numclwwlk5  30458  minvecolem5  30952  ocsh  31354  shless  31430  leopadd  32203  leopmuli  32204  leopmul2i  32206  leoptr  32208  spansncv2  32364  mdsl0  32381  ssdmd1  32384  cvdmd  32408  cdj3i  32512  uzssico  32857  expgt0b  32890  eqgvscpbl  33410  qusvscpbl  33411  cmpcref  33994  acycgrsubgr  35340  cvmliftmolem1  35463  satffunlem2lem2  35588  mrsubff1  35696  msubff1  35738  lediv2aALT  35859  cgr3tr4  36234  colinearxfr  36257  lineext  36258  brsegle  36290  seglecgr12im  36292  segletr  36296  colinbtwnle  36300  outsideoftr  36311  lineelsb2  36330  ivthALT  36517  tailfb  36559  poimirlem29  37970  itg2addnclem  37992  itg2addnclem3  37994  itg2addnc  37995  incsequz  38069  mettrifi  38078  ismtycnv  38123  bfplem1  38143  ghomco  38212  rngoisocnv  38302  keridl  38353  dmncan1  38397  ax12indalem  39391  ax12inda2ALT  39392  omllaw4  39692  cmtcomlemN  39694  cvlexch2  39775  cvlatexch2  39783  cvrexch  39866  atexchltN  39887  3atlem5  39933  lplnribN  39997  linepsubN  40198  paddss1  40263  paddss2  40264  pmapjoin  40298  pmapjat1  40299  cdleme36a  40906  dib2dim  41689  dih2dimbALTN  41691  djhcvat42  41861  dihjatcclem4  41867  dihjat1lem  41874  lcfrlem6  41993  hlhillcs  42404  oexpreposd  42754  mulgt0b1d  42917  mullt0b1d  42928  pell1234qrmulcl  43283  pell14qrss1234  43284  pell14qrmulcl  43291  pell14qrreccl  43292  pell1qrss14  43296  monotoddzzfi  43370  oddcomabszz  43372  omabs2  43760  omcl3g  43762  tfsconcat0b  43774  naddwordnexlem4  43829  climinf  46036  2ffzoeq  47776  iccpartgt  47887  pgnbgreunbgrlem1  48589  pgnbgreunbgrlem4  48595  upwlkwlk  48615  uspgrsprf1  48623  rrx2xpref1o  49194  itschlc0yqe  49236  resipos  49450