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  4673  unielrel  6229  predtrss  6277  fvrnressn  7103  fconst5  7149  soisores  7270  caofrss  7658  caoftrn  7660  f1o2ndf1  8061  oaord  8471  omord2  8491  omcan  8493  oeord  8512  oecan  8513  nnaord  8543  nnmord  8556  omsmo  8582  pmss12g  8803  cantnf  9594  pm54.43  9905  ttukeylem2  10412  axlttrn  11196  axltadd  11197  axmulgt0  11198  axsup  11199  ltadd2  11228  ltord1  11654  recex  11760  ltmul1  11982  lt2msq  12018  nnge1  12164  zltp1le  12532  uzss  12765  eluzp1m1  12768  prodge0rd  13005  ixxssixx  13266  zesq  14140  pfxccatin12lem3  14646  swrdccat3blem  14653  relexpsucnnr  14939  climrlim2  15461  rlimres  15472  climshftlem  15488  lo1add  15541  lo1mul  15542  rlimsqzlem  15563  lo1le  15566  isercolllem2  15580  isercoll  15582  climsup  15584  cvgcmp  15730  climcndslem1  15763  dvds1lem  16185  sumodd  16306  rprpwr  16477  algcvg  16494  eucalgcvga  16504  rpexp12i  16642  crth  16696  pc2dvds  16798  pcmpt  16811  prmpwdvds  16823  1arith  16846  vdwlem2  16901  vdwlem6  16905  vdwlem8  16907  ercpbl  17461  initoid  17916  termoid  17917  ipopos  18450  insubm  18734  subginv  19054  symggrp  19320  f1otrspeq  19367  lsmless1x  19564  lsmless2x  19565  dprdss  19951  rngpropd  20100  dvdsunit  20306  irredrmul  20354  isdrngd  20689  isdrngdOLD  20691  lspextmo  20999  rngqiprngimf1lem  21240  domnchr  21478  zntoslem  21502  evlseu  22029  mat2pmatf1  22664  tgss  22903  neips  23048  opnnei  23055  lpss3  23079  ssrest  23111  t1t0  23283  kgen2ss  23490  isfild  23793  fgss  23808  fgss2  23809  cnpflf2  23935  fclsss1  23957  fclsss2  23958  tgpt0  24054  tsmsxp  24090  prdsxmslem2  24464  ngptgp  24571  nghmcn  24680  qdensere  24704  evth  24905  nmhmcn  25067  tcphcph  25184  caussi  25244  equivcfil  25246  rrxmvallem  25351  ivthlem2  25400  ovollb2lem  25436  ovolunlem1  25445  volun  25493  ioombl1lem4  25509  volsup2  25553  volcn  25554  ismbf3d  25602  itg2mulclem  25694  cpnord  25884  lhop1  25966  aaliou3lem2  26298  ulmclm  26343  ulmss  26353  abelth  26398  cosord  26487  efif1olem4  26501  argimgt0  26568  logdivlt  26577  cxploglim  26935  dvdssqf  27095  mumullem1  27136  mumullem2  27137  bposlem6  27247  lgsdchr  27313  gausslemma2dlem1a  27323  m1lgs  27346  chtppilim  27433  sletr  27717  sletric  27723  madebdayim  27853  madebdaylemold  27863  sltlpss  27873  om2noseqf1o  28251  zsoring  28352  ax5seg  28937  axpasch  28940  axlowdimlem16  28956  axeuclid  28962  axcontlem4  28966  usgr1v0e  29325  nb3gr2nb  29383  cplgr1v  29429  finsumvtxdg2size  29550  usgr2pthlem  29762  clwwlknwwlksn  30039  erclwwlknsym  30071  erclwwlkntr  30072  frgr3vlem1  30274  3vfriswmgrlem  30278  numclwwlk5  30389  minvecolem5  30882  ocsh  31284  shless  31360  leopadd  32133  leopmuli  32134  leopmul2i  32136  leoptr  32138  spansncv2  32294  mdsl0  32311  ssdmd1  32314  cvdmd  32338  cdj3i  32442  uzssico  32792  expgt0b  32825  eqgvscpbl  33359  qusvscpbl  33360  cmpcref  33935  acycgrsubgr  35274  cvmliftmolem1  35397  satffunlem2lem2  35522  mrsubff1  35630  msubff1  35672  lediv2aALT  35793  cgr3tr4  36168  colinearxfr  36191  lineext  36192  brsegle  36224  seglecgr12im  36226  segletr  36230  colinbtwnle  36234  outsideoftr  36245  lineelsb2  36264  ivthALT  36451  tailfb  36493  poimirlem29  37762  itg2addnclem  37784  itg2addnclem3  37786  itg2addnc  37787  incsequz  37861  mettrifi  37870  ismtycnv  37915  bfplem1  37935  ghomco  38004  rngoisocnv  38094  keridl  38145  dmncan1  38189  ax12indalem  39117  ax12inda2ALT  39118  omllaw4  39418  cmtcomlemN  39420  cvlexch2  39501  cvlatexch2  39509  cvrexch  39592  atexchltN  39613  3atlem5  39659  lplnribN  39723  linepsubN  39924  paddss1  39989  paddss2  39990  pmapjoin  40024  pmapjat1  40025  cdleme36a  40632  dib2dim  41415  dih2dimbALTN  41417  djhcvat42  41587  dihjatcclem4  41593  dihjat1lem  41600  lcfrlem6  41719  hlhillcs  42130  oexpreposd  42492  mulgt0b1d  42642  mullt0b1d  42653  pell1234qrmulcl  43012  pell14qrss1234  43013  pell14qrmulcl  43020  pell14qrreccl  43021  pell1qrss14  43025  monotoddzzfi  43099  oddcomabszz  43101  omabs2  43489  omcl3g  43491  tfsconcat0b  43503  naddwordnexlem4  43558  climinf  45768  2ffzoeq  47489  iccpartgt  47589  pgnbgreunbgrlem1  48275  pgnbgreunbgrlem4  48281  upwlkwlk  48301  uspgrsprf1  48309  rrx2xpref1o  48880  itschlc0yqe  48922  resipos  49136