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 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  4656  unielrel  6181  predtrss  6229  fvrnressn  7042  fconst5  7090  soisores  7207  caofrss  7578  caoftrn  7580  f1o2ndf1  7972  oaord  8387  omord2  8407  omcan  8409  oeord  8428  oecan  8429  nnaord  8459  nnmord  8472  omsmo  8497  pmss12g  8666  cantnf  9460  pm54.43  9768  ttukeylem2  10275  axlttrn  11056  axltadd  11057  axmulgt0  11058  axsup  11059  ltadd2  11088  ltord1  11510  recex  11616  ltmul1  11834  lt2msq  11869  nnge1  12010  zltp1le  12379  uzss  12614  eluzp1m1  12617  prodge0rd  12846  ixxssixx  13102  zesq  13950  pfxccatin12lem3  14454  swrdccat3blem  14461  relexpsucnnr  14745  climrlim2  15265  rlimres  15276  climshftlem  15292  lo1add  15345  lo1mul  15346  rlimsqzlem  15369  lo1le  15372  isercolllem2  15386  isercoll  15388  climsup  15390  cvgcmp  15537  climcndslem1  15570  dvds1lem  15986  sumodd  16106  rprpwr  16277  algcvg  16290  eucalgcvga  16300  rpexp12i  16438  crth  16488  pc2dvds  16589  pcmpt  16602  prmpwdvds  16614  1arith  16637  vdwlem2  16692  vdwlem6  16696  vdwlem8  16698  ercpbl  17269  initoid  17725  termoid  17726  ipopos  18263  insubm  18466  subginv  18771  symggrp  19017  f1otrspeq  19064  lsmless1x  19258  lsmless2x  19259  dprdss  19641  dvdsunit  19914  irredrmul  19958  isdrngd  20025  lspextmo  20327  domnchr  20745  zntoslem  20773  evlseu  21302  mat2pmatf1  21887  tgss  22127  neips  22273  opnnei  22280  lpss3  22304  ssrest  22336  t1t0  22508  kgen2ss  22715  isfild  23018  fgss  23033  fgss2  23034  cnpflf2  23160  fclsss1  23182  fclsss2  23183  tgpt0  23279  tsmsxp  23315  prdsxmslem2  23694  ngptgp  23801  nghmcn  23918  qdensere  23942  evth  24131  nmhmcn  24292  tcphcph  24410  caussi  24470  equivcfil  24472  rrxmvallem  24577  ivthlem2  24625  ovollb2lem  24661  ovolunlem1  24670  volun  24718  ioombl1lem4  24734  volsup2  24778  volcn  24779  ismbf3d  24827  itg2mulclem  24920  cpnord  25108  lhop1  25187  aaliou3lem2  25512  ulmclm  25555  ulmss  25565  abelth  25609  cosord  25696  efif1olem4  25710  argimgt0  25776  logdivlt  25785  cxploglim  26136  dvdssqf  26296  mumullem1  26337  mumullem2  26338  bposlem6  26446  lgsdchr  26512  gausslemma2dlem1a  26522  m1lgs  26545  chtppilim  26632  ax5seg  27315  axpasch  27318  axlowdimlem16  27334  axeuclid  27340  axcontlem4  27344  usgr1v0e  27702  nb3gr2nb  27760  cplgr1v  27806  finsumvtxdg2size  27926  usgr2pthlem  28140  clwwlknwwlksn  28411  erclwwlknsym  28443  erclwwlkntr  28444  frgr3vlem1  28646  3vfriswmgrlem  28650  numclwwlk5  28761  minvecolem5  29252  ocsh  29654  shless  29730  leopadd  30503  leopmuli  30504  leopmul2i  30506  leoptr  30508  spansncv2  30664  mdsl0  30681  ssdmd1  30684  cvdmd  30708  cdj3i  30812  uzssico  31114  eqgvscpbl  31559  qusvscpbl  31560  cmpcref  31809  acycgrsubgr  33129  cvmliftmolem1  33252  satffunlem2lem2  33377  mrsubff1  33485  msubff1  33527  lediv2aALT  33644  sletr  33970  madebdayim  34079  madebdaylemold  34087  sltlpss  34096  cgr3tr4  34363  colinearxfr  34386  lineext  34387  brsegle  34419  seglecgr12im  34421  segletr  34425  colinbtwnle  34429  outsideoftr  34440  lineelsb2  34459  ivthALT  34533  tailfb  34575  poimirlem29  35815  itg2addnclem  35837  itg2addnclem3  35839  itg2addnc  35840  incsequz  35915  mettrifi  35924  ismtycnv  35969  bfplem1  35989  ghomco  36058  rngoisocnv  36148  keridl  36199  dmncan1  36243  ax12indalem  36966  ax12inda2ALT  36967  omllaw4  37267  cmtcomlemN  37269  cvlexch2  37350  cvlatexch2  37358  cvrexch  37441  atexchltN  37462  3atlem5  37508  lplnribN  37572  linepsubN  37773  paddss1  37838  paddss2  37839  pmapjoin  37873  pmapjat1  37874  cdleme36a  38481  dib2dim  39264  dih2dimbALTN  39266  djhcvat42  39436  dihjatcclem4  39442  dihjat1lem  39449  lcfrlem6  39568  hlhillcs  39983  oexpreposd  40328  mulgt0b2d  40437  pell1234qrmulcl  40684  pell14qrss1234  40685  pell14qrmulcl  40692  pell14qrreccl  40693  pell1qrss14  40697  monotoddzzfi  40771  oddcomabszz  40773  climinf  43154  2ffzoeq  44831  iccpartgt  44890  upwlkwlk  45312  uspgrsprf1  45320  rrx2xpref1o  46075  itschlc0yqe  46117