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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  rmosn  4687  unielrel  6278  predtrss  6327  fvrnressn  7162  fconst5  7208  soisores  7331  caofrss  7719  caoftrn  7721  f1o2ndf1  8119  oaord  8534  omord2  8554  omcan  8556  oeord  8576  oecan  8577  nnaord  8607  nnmord  8620  omsmo  8646  pmss12g  8869  cantnf  9665  pm54.43  9999  ttukeylem2  10505  axlttrn  11293  axltadd  11294  axmulgt0  11295  axsup  11296  ltadd2  11325  ltord1  11751  recex  11857  ltmul1  12076  lt2msq  12111  nnge1  12275  zltp1le  12655  uzss  12897  eluzp1m1  12900  prodge0rd  13137  ixxssixx  13398  zesq  14276  pfxccatin12lem3  14787  swrdccat3blem  14794  relexpsucnnr  15082  climrlim2  15618  rlimres  15629  climshftlem  15645  lo1add  15698  lo1mul  15699  rlimsqzlem  15720  lo1le  15723  isercolllem2  15737  isercoll  15739  climsup  15741  cvgcmp  15887  climcndslem1  15922  dvds1lem  16343  sumodd  16464  rprpwr  16635  algcvg  16652  eucalgcvga  16662  rpexp12i  16801  crth  16855  pc2dvds  16957  pcmpt  16970  prmpwdvds  16982  1arith  17005  vdwlem2  17060  vdwlem6  17064  vdwlem8  17066  ercpbl  17621  initoid  18076  termoid  18077  ipopos  18610  insubm  18901  subginv  19223  symggrp  19494  f1otrspeq  19541  lsmless1x  19738  lsmless2x  19739  dprdss  20125  rngpropd  20276  dvdsunit  20487  irredrmul  20535  isdrngd  20898  isdrngdOLD  20900  lspextmo  21207  rngqiprngimf1lem  21464  domnchr  21712  zntoslem  21736  evlseu  22264  mat2pmatf1  22916  tgss  23155  neips  23300  opnnei  23307  lpss3  23331  ssrest  23363  t1t0  23535  kgen2ss  23743  isfild  24046  fgss  24061  fgss2  24062  cnpflf2  24188  fclsss1  24210  fclsss2  24211  tgpt0  24307  tsmsxp  24343  prdsxmslem2  24717  ngptgp  24824  nghmcn  24933  qdensere  24957  evth  25149  nmhmcn  25310  tcphcph  25427  caussi  25487  equivcfil  25489  rrxmvallem  25594  ivthlem2  25642  ovollb2lem  25678  ovolunlem1  25687  volun  25735  ioombl1lem4  25751  volsup2  25795  volcn  25796  ismbf3d  25844  itg2mulclem  25936  cpnord  26125  lhop1  26204  aaliou3lem2  26537  ulmclm  26581  ulmss  26591  abelth  26635  cosord  26727  efif1olem4  26741  argimgt0  26808  logdivlt  26817  cxploglim  27173  dvdssqf  27333  mumullem1  27374  mumullem2  27375  bposlem6  27484  lgsdchr  27550  gausslemma2dlem1a  27560  m1lgs  27583  chtppilim  27670  lestr  27957  lestric  27963  madebdayim  28112  madebdaylemold  28122  ltslpss  28132  om2noseqf1o  28525  zsoring  28633  bdaypw2n0bndlem  28687  bdayfin  28711  ax5seg  29319  axpasch  29322  axlowdimlem16  29338  axeuclid  29344  axcontlem4  29348  usgr1v0e  29710  nb3gr2nb  29768  cplgr1v  29814  finsumvtxdg2size  29934  usgr2pthlem  30152  clwwlknwwlksn  30432  erclwwlknsym  30464  erclwwlkntr  30465  frgr3vlem1  30671  3vfriswmgrlem  30675  numclwwlk5  30786  minvecolem5  31280  ocsh  31682  shless  31758  leopadd  32531  leopmuli  32532  leopmul2i  32534  leoptr  32536  spansncv2  32692  mdsl0  32709  ssdmd1  32712  cvdmd  32736  cdj3i  32840  uzssico  33175  expgt0b  33207  eqgvscpbl  33710  qusvscpbl  33711  cmpcref  34280  acycgrsubgr  35663  cvmliftmolem1  35786  satffunlem2lem2  35911  mrsubff1  36019  msubff1  36061  lediv2aALT  36182  cgr3tr4  36557  colinearxfr  36580  lineext  36581  brsegle  36613  seglecgr12im  36615  segletr  36619  colinbtwnle  36623  outsideoftr  36634  lineelsb2  36653  ltnmul  36721  ltnadd  36723  ivthALT  36879  tailfb  36921  poimirlem29  38333  itg2addnclem  38355  itg2addnclem3  38357  itg2addnc  38358  incsequz  38432  mettrifi  38441  ismtycnv  38486  bfplem1  38506  ghomco  38575  rngoisocnv  38665  keridl  38716  dmncan1  38760  ax12indalem  39752  ax12inda2ALT  39753  omllaw4  40053  cmtcomlemN  40055  cvlexch2  40136  cvlatexch2  40144  cvrexch  40227  atexchltN  40248  3atlem5  40294  lplnribN  40358  linepsubN  40559  paddss1  40624  paddss2  40625  pmapjoin  40659  pmapjat1  40660  cdleme36a  41267  dib2dim  42050  dih2dimbALTN  42052  djhcvat42  42222  dihjatcclem4  42228  dihjat1lem  42235  lcfrlem6  42354  hlhillcs  42765  oexpreposd  43116  mulgt0b1d  43279  mullt0b1d  43290  pell1234qrmulcl  43615  pell14qrss1234  43616  pell14qrmulcl  43623  pell14qrreccl  43624  pell1qrss14  43628  monotoddzzfi  43702  oddcomabszz  43704  omabs2  44092  omcl3g  44094  tfsconcat0b  44106  naddwordnexlem4  44161  climinf  46355  2ffzoeq  48098  iccpartgt  48209  pgnbgreunbgrlem1  48911  pgnbgreunbgrlem4  48917  upwlkwlk  48937  uspgrsprf1  48945  idomcanl  49145  rrx2xpref1o  49531  itschlc0yqe  49573  resipos  49786