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  4679  unielrel  6235  predtrss  6283  fvrnressn  7115  fconst5  7162  soisores  7284  caofrss  7672  caoftrn  7674  f1o2ndf1  8078  oaord  8488  omord2  8508  omcan  8510  oeord  8529  oecan  8530  nnaord  8560  nnmord  8573  omsmo  8599  pmss12g  8819  cantnf  9622  pm54.43  9930  ttukeylem2  10439  axlttrn  11222  axltadd  11223  axmulgt0  11224  axsup  11225  ltadd2  11254  ltord1  11680  recex  11786  ltmul1  12008  lt2msq  12044  nnge1  12190  zltp1le  12559  uzss  12792  eluzp1m1  12795  prodge0rd  13036  ixxssixx  13296  zesq  14167  pfxccatin12lem3  14673  swrdccat3blem  14680  relexpsucnnr  14967  climrlim2  15489  rlimres  15500  climshftlem  15516  lo1add  15569  lo1mul  15570  rlimsqzlem  15591  lo1le  15594  isercolllem2  15608  isercoll  15610  climsup  15612  cvgcmp  15758  climcndslem1  15791  dvds1lem  16213  sumodd  16334  rprpwr  16505  algcvg  16522  eucalgcvga  16532  rpexp12i  16670  crth  16724  pc2dvds  16826  pcmpt  16839  prmpwdvds  16851  1arith  16874  vdwlem2  16929  vdwlem6  16933  vdwlem8  16935  ercpbl  17488  initoid  17939  termoid  17940  ipopos  18471  insubm  18721  subginv  19041  symggrp  19306  f1otrspeq  19353  lsmless1x  19550  lsmless2x  19551  dprdss  19937  rngpropd  20059  dvdsunit  20264  irredrmul  20312  isdrngd  20650  isdrngdOLD  20652  lspextmo  20939  rngqiprngimf1lem  21180  domnchr  21418  zntoslem  21442  evlseu  21966  mat2pmatf1  22592  tgss  22831  neips  22976  opnnei  22983  lpss3  23007  ssrest  23039  t1t0  23211  kgen2ss  23418  isfild  23721  fgss  23736  fgss2  23737  cnpflf2  23863  fclsss1  23885  fclsss2  23886  tgpt0  23982  tsmsxp  24018  prdsxmslem2  24393  ngptgp  24500  nghmcn  24609  qdensere  24633  evth  24834  nmhmcn  24996  tcphcph  25113  caussi  25173  equivcfil  25175  rrxmvallem  25280  ivthlem2  25329  ovollb2lem  25365  ovolunlem1  25374  volun  25422  ioombl1lem4  25438  volsup2  25482  volcn  25483  ismbf3d  25531  itg2mulclem  25623  cpnord  25813  lhop1  25895  aaliou3lem2  26227  ulmclm  26272  ulmss  26282  abelth  26327  cosord  26416  efif1olem4  26430  argimgt0  26497  logdivlt  26506  cxploglim  26864  dvdssqf  27024  mumullem1  27065  mumullem2  27066  bposlem6  27176  lgsdchr  27242  gausslemma2dlem1a  27252  m1lgs  27275  chtppilim  27362  sletr  27646  sletric  27652  madebdayim  27775  madebdaylemold  27785  sltlpss  27795  om2noseqf1o  28171  ax5seg  28841  axpasch  28844  axlowdimlem16  28860  axeuclid  28866  axcontlem4  28870  usgr1v0e  29229  nb3gr2nb  29287  cplgr1v  29333  finsumvtxdg2size  29454  usgr2pthlem  29666  clwwlknwwlksn  29940  erclwwlknsym  29972  erclwwlkntr  29973  frgr3vlem1  30175  3vfriswmgrlem  30179  numclwwlk5  30290  minvecolem5  30783  ocsh  31185  shless  31261  leopadd  32034  leopmuli  32035  leopmul2i  32037  leoptr  32039  spansncv2  32195  mdsl0  32212  ssdmd1  32215  cvdmd  32239  cdj3i  32343  uzssico  32680  expgt0b  32714  eqgvscpbl  33294  qusvscpbl  33295  cmpcref  33813  acycgrsubgr  35118  cvmliftmolem1  35241  satffunlem2lem2  35366  mrsubff1  35474  msubff1  35516  lediv2aALT  35637  cgr3tr4  36013  colinearxfr  36036  lineext  36037  brsegle  36069  seglecgr12im  36071  segletr  36075  colinbtwnle  36079  outsideoftr  36090  lineelsb2  36109  ivthALT  36296  tailfb  36338  poimirlem29  37616  itg2addnclem  37638  itg2addnclem3  37640  itg2addnc  37641  incsequz  37715  mettrifi  37724  ismtycnv  37769  bfplem1  37789  ghomco  37858  rngoisocnv  37948  keridl  37999  dmncan1  38043  ax12indalem  38911  ax12inda2ALT  38912  omllaw4  39212  cmtcomlemN  39214  cvlexch2  39295  cvlatexch2  39303  cvrexch  39387  atexchltN  39408  3atlem5  39454  lplnribN  39518  linepsubN  39719  paddss1  39784  paddss2  39785  pmapjoin  39819  pmapjat1  39820  cdleme36a  40427  dib2dim  41210  dih2dimbALTN  41212  djhcvat42  41382  dihjatcclem4  41388  dihjat1lem  41395  lcfrlem6  41514  hlhillcs  41925  oexpreposd  42283  mulgt0b1d  42433  mullt0b1d  42444  pell1234qrmulcl  42816  pell14qrss1234  42817  pell14qrmulcl  42824  pell14qrreccl  42825  pell1qrss14  42829  monotoddzzfi  42904  oddcomabszz  42906  omabs2  43294  omcl3g  43296  tfsconcat0b  43308  naddwordnexlem4  43363  climinf  45577  2ffzoeq  47301  iccpartgt  47401  pgnbgreunbgrlem1  48076  pgnbgreunbgrlem4  48082  upwlkwlk  48100  uspgrsprf1  48108  rrx2xpref1o  48680  itschlc0yqe  48722  resipos  48936