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  6226  predtrss  6274  fvrnressn  7099  fconst5  7146  soisores  7268  caofrss  7656  caoftrn  7658  f1o2ndf1  8062  oaord  8472  omord2  8492  omcan  8494  oeord  8513  oecan  8514  nnaord  8544  nnmord  8557  omsmo  8583  pmss12g  8803  cantnf  9608  pm54.43  9916  ttukeylem2  10423  axlttrn  11207  axltadd  11208  axmulgt0  11209  axsup  11210  ltadd2  11239  ltord1  11665  recex  11771  ltmul1  11993  lt2msq  12029  nnge1  12175  zltp1le  12544  uzss  12777  eluzp1m1  12780  prodge0rd  13021  ixxssixx  13281  zesq  14152  pfxccatin12lem3  14657  swrdccat3blem  14664  relexpsucnnr  14951  climrlim2  15473  rlimres  15484  climshftlem  15500  lo1add  15553  lo1mul  15554  rlimsqzlem  15575  lo1le  15578  isercolllem2  15592  isercoll  15594  climsup  15596  cvgcmp  15742  climcndslem1  15775  dvds1lem  16197  sumodd  16318  rprpwr  16489  algcvg  16506  eucalgcvga  16516  rpexp12i  16654  crth  16708  pc2dvds  16810  pcmpt  16823  prmpwdvds  16835  1arith  16858  vdwlem2  16913  vdwlem6  16917  vdwlem8  16919  ercpbl  17472  initoid  17927  termoid  17928  ipopos  18461  insubm  18711  subginv  19031  symggrp  19298  f1otrspeq  19345  lsmless1x  19542  lsmless2x  19543  dprdss  19929  rngpropd  20078  dvdsunit  20283  irredrmul  20331  isdrngd  20669  isdrngdOLD  20671  lspextmo  20979  rngqiprngimf1lem  21220  domnchr  21458  zntoslem  21482  evlseu  22007  mat2pmatf1  22633  tgss  22872  neips  23017  opnnei  23024  lpss3  23048  ssrest  23080  t1t0  23252  kgen2ss  23459  isfild  23762  fgss  23777  fgss2  23778  cnpflf2  23904  fclsss1  23926  fclsss2  23927  tgpt0  24023  tsmsxp  24059  prdsxmslem2  24434  ngptgp  24541  nghmcn  24650  qdensere  24674  evth  24875  nmhmcn  25037  tcphcph  25154  caussi  25214  equivcfil  25216  rrxmvallem  25321  ivthlem2  25370  ovollb2lem  25406  ovolunlem1  25415  volun  25463  ioombl1lem4  25479  volsup2  25523  volcn  25524  ismbf3d  25572  itg2mulclem  25664  cpnord  25854  lhop1  25936  aaliou3lem2  26268  ulmclm  26313  ulmss  26323  abelth  26368  cosord  26457  efif1olem4  26471  argimgt0  26538  logdivlt  26547  cxploglim  26905  dvdssqf  27065  mumullem1  27106  mumullem2  27107  bposlem6  27217  lgsdchr  27283  gausslemma2dlem1a  27293  m1lgs  27316  chtppilim  27403  sletr  27687  sletric  27693  madebdayim  27821  madebdaylemold  27831  sltlpss  27841  om2noseqf1o  28219  zsoring  28320  ax5seg  28902  axpasch  28905  axlowdimlem16  28921  axeuclid  28927  axcontlem4  28931  usgr1v0e  29290  nb3gr2nb  29348  cplgr1v  29394  finsumvtxdg2size  29515  usgr2pthlem  29727  clwwlknwwlksn  30001  erclwwlknsym  30033  erclwwlkntr  30034  frgr3vlem1  30236  3vfriswmgrlem  30240  numclwwlk5  30351  minvecolem5  30844  ocsh  31246  shless  31322  leopadd  32095  leopmuli  32096  leopmul2i  32098  leoptr  32100  spansncv2  32256  mdsl0  32273  ssdmd1  32276  cvdmd  32300  cdj3i  32404  uzssico  32746  expgt0b  32780  eqgvscpbl  33306  qusvscpbl  33307  cmpcref  33836  acycgrsubgr  35150  cvmliftmolem1  35273  satffunlem2lem2  35398  mrsubff1  35506  msubff1  35548  lediv2aALT  35669  cgr3tr4  36045  colinearxfr  36068  lineext  36069  brsegle  36101  seglecgr12im  36103  segletr  36107  colinbtwnle  36111  outsideoftr  36122  lineelsb2  36141  ivthALT  36328  tailfb  36370  poimirlem29  37648  itg2addnclem  37670  itg2addnclem3  37672  itg2addnc  37673  incsequz  37747  mettrifi  37756  ismtycnv  37801  bfplem1  37821  ghomco  37890  rngoisocnv  37980  keridl  38031  dmncan1  38075  ax12indalem  38943  ax12inda2ALT  38944  omllaw4  39244  cmtcomlemN  39246  cvlexch2  39327  cvlatexch2  39335  cvrexch  39419  atexchltN  39440  3atlem5  39486  lplnribN  39550  linepsubN  39751  paddss1  39816  paddss2  39817  pmapjoin  39851  pmapjat1  39852  cdleme36a  40459  dib2dim  41242  dih2dimbALTN  41244  djhcvat42  41414  dihjatcclem4  41420  dihjat1lem  41427  lcfrlem6  41546  hlhillcs  41957  oexpreposd  42315  mulgt0b1d  42465  mullt0b1d  42476  pell1234qrmulcl  42848  pell14qrss1234  42849  pell14qrmulcl  42856  pell14qrreccl  42857  pell1qrss14  42861  monotoddzzfi  42935  oddcomabszz  42937  omabs2  43325  omcl3g  43327  tfsconcat0b  43339  naddwordnexlem4  43394  climinf  45607  2ffzoeq  47331  iccpartgt  47431  pgnbgreunbgrlem1  48117  pgnbgreunbgrlem4  48123  upwlkwlk  48143  uspgrsprf1  48151  rrx2xpref1o  48723  itschlc0yqe  48765  resipos  48979