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

Syntax hints:   → wi 4   ↔ wb 205

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 206

This theorem is referenced by:  rmosn  4724  unielrel  6274  predtrss  6324  fvrnressn  7159  fconst5  7207  soisores  7324  caofrss  7706  caoftrn  7708  f1o2ndf1  8108  oaord  8547  omord2  8567  omcan  8569  oeord  8588  oecan  8589  nnaord  8619  nnmord  8632  omsmo  8657  pmss12g  8863  cantnf  9688  pm54.43  9996  ttukeylem2  10505  axlttrn  11286  axltadd  11287  axmulgt0  11288  axsup  11289  ltadd2  11318  ltord1  11740  recex  11846  ltmul1  12064  lt2msq  12099  nnge1  12240  zltp1le  12612  uzss  12845  eluzp1m1  12848  prodge0rd  13081  ixxssixx  13338  zesq  14189  pfxccatin12lem3  14682  swrdccat3blem  14689  relexpsucnnr  14972  climrlim2  15491  rlimres  15502  climshftlem  15518  lo1add  15571  lo1mul  15572  rlimsqzlem  15595  lo1le  15598  isercolllem2  15612  isercoll  15614  climsup  15616  cvgcmp  15762  climcndslem1  15795  dvds1lem  16211  sumodd  16331  rprpwr  16500  algcvg  16513  eucalgcvga  16523  rpexp12i  16661  crth  16711  pc2dvds  16812  pcmpt  16825  prmpwdvds  16837  1arith  16860  vdwlem2  16915  vdwlem6  16919  vdwlem8  16921  ercpbl  17495  initoid  17951  termoid  17952  ipopos  18489  insubm  18699  subginv  19013  symggrp  19268  f1otrspeq  19315  lsmless1x  19512  lsmless2x  19513  dprdss  19899  dvdsunit  20193  irredrmul  20241  isdrngd  20390  isdrngdOLD  20392  lspextmo  20667  domnchr  21084  zntoslem  21112  evlseu  21646  mat2pmatf1  22231  tgss  22471  neips  22617  opnnei  22624  lpss3  22648  ssrest  22680  t1t0  22852  kgen2ss  23059  isfild  23362  fgss  23377  fgss2  23378  cnpflf2  23504  fclsss1  23526  fclsss2  23527  tgpt0  23623  tsmsxp  23659  prdsxmslem2  24038  ngptgp  24145  nghmcn  24262  qdensere  24286  evth  24475  nmhmcn  24636  tcphcph  24754  caussi  24814  equivcfil  24816  rrxmvallem  24921  ivthlem2  24969  ovollb2lem  25005  ovolunlem1  25014  volun  25062  ioombl1lem4  25078  volsup2  25122  volcn  25123  ismbf3d  25171  itg2mulclem  25264  cpnord  25452  lhop1  25531  aaliou3lem2  25856  ulmclm  25899  ulmss  25909  abelth  25953  cosord  26040  efif1olem4  26054  argimgt0  26120  logdivlt  26129  cxploglim  26482  dvdssqf  26642  mumullem1  26683  mumullem2  26684  bposlem6  26792  lgsdchr  26858  gausslemma2dlem1a  26868  m1lgs  26891  chtppilim  26978  sletr  27261  sletric  27267  madebdayim  27382  madebdaylemold  27392  sltlpss  27401  ax5seg  28196  axpasch  28199  axlowdimlem16  28215  axeuclid  28221  axcontlem4  28225  usgr1v0e  28583  nb3gr2nb  28641  cplgr1v  28687  finsumvtxdg2size  28807  usgr2pthlem  29020  clwwlknwwlksn  29291  erclwwlknsym  29323  erclwwlkntr  29324  frgr3vlem1  29526  3vfriswmgrlem  29530  numclwwlk5  29641  minvecolem5  30134  ocsh  30536  shless  30612  leopadd  31385  leopmuli  31386  leopmul2i  31388  leoptr  31390  spansncv2  31546  mdsl0  31563  ssdmd1  31566  cvdmd  31590  cdj3i  31694  uzssico  31995  eqgvscpbl  32465  qusvscpbl  32466  cmpcref  32830  acycgrsubgr  34149  cvmliftmolem1  34272  satffunlem2lem2  34397  mrsubff1  34505  msubff1  34547  lediv2aALT  34662  cgr3tr4  35024  colinearxfr  35047  lineext  35048  brsegle  35080  seglecgr12im  35082  segletr  35086  colinbtwnle  35090  outsideoftr  35101  lineelsb2  35120  ivthALT  35220  tailfb  35262  poimirlem29  36517  itg2addnclem  36539  itg2addnclem3  36541  itg2addnc  36542  incsequz  36616  mettrifi  36625  ismtycnv  36670  bfplem1  36690  ghomco  36759  rngoisocnv  36849  keridl  36900  dmncan1  36944  ax12indalem  37815  ax12inda2ALT  37816  omllaw4  38116  cmtcomlemN  38118  cvlexch2  38199  cvlatexch2  38207  cvrexch  38291  atexchltN  38312  3atlem5  38358  lplnribN  38422  linepsubN  38623  paddss1  38688  paddss2  38689  pmapjoin  38723  pmapjat1  38724  cdleme36a  39331  dib2dim  40114  dih2dimbALTN  40116  djhcvat42  40286  dihjatcclem4  40292  dihjat1lem  40299  lcfrlem6  40418  hlhillcs  40833  oexpreposd  41212  mulgt0b2d  41333  pell1234qrmulcl  41593  pell14qrss1234  41594  pell14qrmulcl  41601  pell14qrreccl  41602  pell1qrss14  41606  monotoddzzfi  41681  oddcomabszz  41683  omabs2  42082  omcl3g  42084  tfsconcat0b  42096  naddwordnexlem4  42152  climinf  44322  2ffzoeq  46036  iccpartgt  46095  upwlkwlk  46517  uspgrsprf1  46525  rngpropd  46673  rngqiprngimf1lem  46779  rrx2xpref1o  47404  itschlc0yqe  47446