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  4676  unielrel  6279  predtrss  6328  fvrnressn  7170  fconst5  7216  soisores  7339  caofrss  7736  caoftrn  7738  f1o2ndf1  8139  oaord  8562  omord2  8582  omcan  8584  oeord  8604  oecan  8605  nnaord  8635  nnmord  8648  omsmo  8674  pmss12g  8904  cantnf  9701  pm54.43  10089  ttukeylem2  10595  axlttrn  11389  axltadd  11390  axmulgt0  11391  axsup  11392  ltadd2  11421  ltord1  11849  recex  11955  ltmul1  12174  lt2msq  12209  nnge1  12373  zltp1le  12753  uzss  12995  eluzp1m1  12998  prodge0rd  13236  ixxssixx  13497  zesq  14377  pfxccatin12lem3  14889  swrdccat3blem  14896  relexpsucnnr  15187  climrlim2  15723  rlimres  15734  climshftlem  15750  lo1add  15803  lo1mul  15804  rlimsqzlem  15825  lo1le  15828  isercolllem2  15842  isercoll  15844  climsup  15846  cvgcmp  15992  climcndslem1  16027  dvds1lem  16446  sumodd  16567  rprpwr  16742  algcvg  16760  eucalgcvga  16770  rpexp12i  16909  crth  16964  pc2dvds  17066  pcmpt  17079  prmpwdvds  17091  1arith  17114  vdwlem2  17169  vdwlem6  17173  vdwlem8  17175  ercpbl  17730  initoid  18185  termoid  18186  ipopos  18719  insubm  19023  subginv  19352  symggrp  19623  f1otrspeq  19670  lsmless1x  19867  lsmless2x  19868  dprdss  20254  rngpropd  20405  dvdsunit  20618  irredrmul  20666  isdrngd  21031  isdrngdOLD  21033  lspextmo  21340  rngqiprngimf1lem  21599  domnchr  21847  zntoslem  21871  evlseu  22401  mat2pmatf1  23056  tgss  23295  neips  23440  opnnei  23447  lpss3  23471  ssrest  23503  t1t0  23675  kgen2ss  23883  isfild  24186  fgss  24201  fgss2  24202  cnpflf2  24328  fclsss1  24350  fclsss2  24351  tgpt0  24447  tsmsxp  24483  prdsxmslem2  24857  ngptgp  24964  nghmcn  25073  qdensere  25097  evth  25289  nmhmcn  25450  tcphcph  25567  caussi  25627  equivcfil  25629  rrxmvallem  25734  ivthlem2  25782  ovollb2lem  25818  ovolunlem1  25827  volun  25875  ioombl1lem4  25891  volsup2  25935  volcn  25936  ismbf3d  25984  itg2mulclem  26076  cpnord  26264  lhop1  26343  aaliou3lem2  26679  ulmclm  26723  ulmss  26733  abelth  26777  cosord  26868  efif1olem4  26882  argimgt0  26949  logdivlt  26958  cxploglim  27314  dvdssqf  27474  mumullem1  27515  mumullem2  27516  bposlem6  27625  lgsdchr  27691  gausslemma2dlem1a  27701  m1lgs  27724  chtppilim  27811  lestr  28128  lestric  28134  madebdayim  28283  madebdaylemold  28293  ltslpss  28303  om2noseqf1o  28696  zsoring  28804  bdaypw2n0bndlem  28858  bdayfin  28882  ax5seg  29525  axpasch  29528  axlowdimlem16  29544  axeuclid  29550  axcontlem4  29554  usgr1v0e  29916  nb3gr2nb  29974  cplgr1v  30020  finsumvtxdg2size  30140  usgr2pthlem  30358  clwwlknwwlksn  30638  erclwwlknsym  30670  erclwwlkntr  30671  frgr3vlem1  30883  3vfriswmgrlem  30887  numclwwlk5  30998  minvecolem5  31492  ocsh  31894  shless  31970  leopadd  32743  leopmuli  32744  leopmul2i  32746  leoptr  32748  spansncv2  32904  mdsl0  32921  ssdmd1  32924  cvdmd  32948  cdj3i  33052  uzssico  33426  expgt0b  33458  eqgvscpbl  33961  qusvscpbl  33962  cmpcref  34532  acycgrsubgr  36003  cvmliftmolem1  36136  satffunlem2lem2  36261  mrsubff1  36369  msubff1  36411  lediv2aALT  36532  cgr3tr4  36913  colinearxfr  36936  lineext  36937  brsegle  36969  seglecgr12im  36971  segletr  36975  colinbtwnle  36979  outsideoftr  36990  lineelsb2  37009  ltnmul  37061  ltnadd  37063  ivthALT  37219  tailfb  37261  poimirlem29  38676  itg2addnclem  38698  itg2addnclem3  38700  itg2addnc  38701  incsequz  38791  mettrifi  38800  ismtycnv  38845  bfplem1  38865  ghomco  38934  rngoisocnv  39024  keridl  39075  dmncan1  39119  ax12indalem  40111  ax12inda2ALT  40112  omllaw4  40412  cmtcomlemN  40414  cvlexch2  40495  cvlatexch2  40503  cvrexch  40586  atexchltN  40607  3atlem5  40653  lplnribN  40717  linepsubN  40918  paddss1  40983  paddss2  40984  pmapjoin  41018  pmapjat1  41019  cdleme36a  41626  dib2dim  42409  dih2dimbALTN  42411  djhcvat42  42581  dihjatcclem4  42587  dihjat1lem  42594  lcfrlem6  42713  hlhillcs  43124  oexpreposd  43488  mulgt0b1d  43645  mullt0b1d  43656  pell1234qrmulcl  43971  pell14qrss1234  43972  pell14qrmulcl  43979  pell14qrreccl  43980  pell1qrss14  43984  monotoddzzfi  44058  oddcomabszz  44060  omabs2  44443  omcl3g  44445  tfsconcat0b  44457  naddwordnexlem4  44512  climinf  46726  2ffzoeq  48506  iccpartgt  48617  pgnbgreunbgrlem1  49319  pgnbgreunbgrlem4  49325  upwlkwlk  49345  uspgrsprf1  49353  idomcanl  49552  itschlc0yqe  49980  resipos  50197