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  4680  unielrel  6271  predtrss  6320  fvrnressn  7158  fconst5  7205  soisores  7328  caofrss  7717  caoftrn  7719  f1o2ndf1  8119  oaord  8534  omord2  8554  omcan  8556  oeord  8576  oecan  8577  nnaord  8607  nnmord  8620  omsmo  8646  pmss12g  8876  cantnf  9672  pm54.43  10006  ttukeylem2  10512  axlttrn  11306  axltadd  11307  axmulgt0  11308  axsup  11309  ltadd2  11338  ltord1  11764  recex  11870  ltmul1  12089  lt2msq  12124  nnge1  12288  zltp1le  12668  uzss  12910  eluzp1m1  12913  prodge0rd  13151  ixxssixx  13412  zesq  14290  pfxccatin12lem3  14801  swrdccat3blem  14808  relexpsucnnr  15098  climrlim2  15634  rlimres  15645  climshftlem  15661  lo1add  15714  lo1mul  15715  rlimsqzlem  15736  lo1le  15739  isercolllem2  15753  isercoll  15755  climsup  15757  cvgcmp  15903  climcndslem1  15938  dvds1lem  16357  sumodd  16478  rprpwr  16649  algcvg  16666  eucalgcvga  16676  rpexp12i  16815  crth  16869  pc2dvds  16971  pcmpt  16984  prmpwdvds  16996  1arith  17019  vdwlem2  17074  vdwlem6  17078  vdwlem8  17080  ercpbl  17635  initoid  18090  termoid  18091  ipopos  18624  insubm  18927  subginv  19256  symggrp  19527  f1otrspeq  19574  lsmless1x  19771  lsmless2x  19772  dprdss  20158  rngpropd  20309  dvdsunit  20520  irredrmul  20568  isdrngd  20931  isdrngdOLD  20933  lspextmo  21240  rngqiprngimf1lem  21497  domnchr  21745  zntoslem  21769  evlseu  22299  mat2pmatf1  22954  tgss  23193  neips  23338  opnnei  23345  lpss3  23369  ssrest  23401  t1t0  23573  kgen2ss  23781  isfild  24084  fgss  24099  fgss2  24100  cnpflf2  24226  fclsss1  24248  fclsss2  24249  tgpt0  24345  tsmsxp  24381  prdsxmslem2  24755  ngptgp  24862  nghmcn  24971  qdensere  24995  evth  25187  nmhmcn  25348  tcphcph  25465  caussi  25525  equivcfil  25527  rrxmvallem  25632  ivthlem2  25680  ovollb2lem  25716  ovolunlem1  25725  volun  25773  ioombl1lem4  25789  volsup2  25833  volcn  25834  ismbf3d  25882  itg2mulclem  25974  cpnord  26162  lhop1  26241  aaliou3lem2  26579  ulmclm  26623  ulmss  26633  abelth  26677  cosord  26768  efif1olem4  26782  argimgt0  26849  logdivlt  26858  cxploglim  27214  dvdssqf  27374  mumullem1  27415  mumullem2  27416  bposlem6  27525  lgsdchr  27591  gausslemma2dlem1a  27601  m1lgs  27624  chtppilim  27711  lestr  27998  lestric  28004  madebdayim  28153  madebdaylemold  28163  ltslpss  28173  om2noseqf1o  28566  zsoring  28674  bdaypw2n0bndlem  28728  bdayfin  28752  ax5seg  29395  axpasch  29398  axlowdimlem16  29414  axeuclid  29420  axcontlem4  29424  usgr1v0e  29786  nb3gr2nb  29844  cplgr1v  29890  finsumvtxdg2size  30010  usgr2pthlem  30228  clwwlknwwlksn  30508  erclwwlknsym  30540  erclwwlkntr  30541  frgr3vlem1  30753  3vfriswmgrlem  30757  numclwwlk5  30868  minvecolem5  31362  ocsh  31764  shless  31840  leopadd  32613  leopmuli  32614  leopmul2i  32616  leoptr  32618  spansncv2  32774  mdsl0  32791  ssdmd1  32794  cvdmd  32818  cdj3i  32922  uzssico  33255  expgt0b  33287  eqgvscpbl  33790  qusvscpbl  33791  cmpcref  34360  acycgrsubgr  35737  cvmliftmolem1  35860  satffunlem2lem2  35985  mrsubff1  36093  msubff1  36135  lediv2aALT  36256  cgr3tr4  36632  colinearxfr  36655  lineext  36656  brsegle  36688  seglecgr12im  36690  segletr  36694  colinbtwnle  36698  outsideoftr  36709  lineelsb2  36728  ltnmul  36796  ltnadd  36798  ivthALT  36954  tailfb  36996  poimirlem29  38398  itg2addnclem  38420  itg2addnclem3  38422  itg2addnc  38423  incsequz  38498  mettrifi  38507  ismtycnv  38552  bfplem1  38572  ghomco  38641  rngoisocnv  38731  keridl  38782  dmncan1  38826  ax12indalem  39818  ax12inda2ALT  39819  omllaw4  40119  cmtcomlemN  40121  cvlexch2  40202  cvlatexch2  40210  cvrexch  40293  atexchltN  40314  3atlem5  40360  lplnribN  40424  linepsubN  40625  paddss1  40690  paddss2  40691  pmapjoin  40725  pmapjat1  40726  cdleme36a  41333  dib2dim  42116  dih2dimbALTN  42118  djhcvat42  42288  dihjatcclem4  42294  dihjat1lem  42301  lcfrlem6  42420  hlhillcs  42831  oexpreposd  43197  mulgt0b1d  43360  mullt0b1d  43371  pell1234qrmulcl  43696  pell14qrss1234  43697  pell14qrmulcl  43704  pell14qrreccl  43705  pell1qrss14  43709  monotoddzzfi  43783  oddcomabszz  43785  omabs2  44173  omcl3g  44175  tfsconcat0b  44187  naddwordnexlem4  44242  climinf  46436  2ffzoeq  48216  iccpartgt  48327  pgnbgreunbgrlem1  49029  pgnbgreunbgrlem4  49035  upwlkwlk  49055  uspgrsprf1  49063  idomcanl  49262  rrx2xpref1o  49648  itschlc0yqe  49690  resipos  49901