Theorem 3imtr4d 296

Description: More general version of 3imtr4i 294. 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 261	. 2 ⊢ (𝜑 → (𝜓 → 𝜏))
5	1, 4	sylbid 242	1 ⊢ (𝜑 → (𝜃 → 𝜏))

Syntax hints:   → wi 4   ↔ wb 208

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 209

This theorem is referenced by:  rmosn  4675  unielrel  6256  predtrss  6304  fvrnressn  7139  fconst5  7185  soisores  7306  caofrss  7694  caoftrn  7696  f1o2ndf1  8095  oaord  8510  omord2  8530  omcan  8532  oeord  8552  oecan  8553  nnaord  8583  nnmord  8596  omsmo  8622  pmss12g  8845  cantnf  9642  pm54.43  9953  ttukeylem2  10461  axlttrn  11249  axltadd  11250  axmulgt0  11251  axsup  11252  ltadd2  11281  ltord1  11707  recex  11813  ltmul1  12035  lt2msq  12071  nnge1  12235  zltp1le  12615  uzss  12856  eluzp1m1  12859  prodge0rd  13096  ixxssixx  13357  zesq  14233  pfxccatin12lem3  14739  swrdccat3blem  14746  relexpsucnnr  15032  climrlim2  15565  rlimres  15576  climshftlem  15592  lo1add  15645  lo1mul  15646  rlimsqzlem  15667  lo1le  15670  isercolllem2  15684  isercoll  15686  climsup  15688  cvgcmp  15835  climcndslem1  15870  dvds1lem  16292  sumodd  16413  rprpwr  16584  algcvg  16601  eucalgcvga  16611  rpexp12i  16750  crth  16804  pc2dvds  16906  pcmpt  16919  prmpwdvds  16931  1arith  16954  vdwlem2  17009  vdwlem6  17013  vdwlem8  17015  ercpbl  17570  initoid  18025  termoid  18026  ipopos  18559  insubm  18843  subginv  19166  symggrp  19431  f1otrspeq  19478  lsmless1x  19675  lsmless2x  19676  dprdss  20062  rngpropd  20211  dvdsunit  20415  irredrmul  20463  isdrngd  20802  isdrngdOLD  20804  lspextmo  21111  rngqiprngimf1lem  21352  domnchr  21572  zntoslem  21596  evlseu  22124  mat2pmatf1  22777  tgss  23016  neips  23161  opnnei  23168  lpss3  23192  ssrest  23224  t1t0  23396  kgen2ss  23603  isfild  23906  fgss  23921  fgss2  23922  cnpflf2  24048  fclsss1  24070  fclsss2  24071  tgpt0  24167  tsmsxp  24203  prdsxmslem2  24577  ngptgp  24684  nghmcn  24793  qdensere  24817  evth  25009  nmhmcn  25170  tcphcph  25287  caussi  25347  equivcfil  25349  rrxmvallem  25454  ivthlem2  25502  ovollb2lem  25538  ovolunlem1  25547  volun  25595  ioombl1lem4  25611  volsup2  25655  volcn  25656  ismbf3d  25704  itg2mulclem  25796  cpnord  25985  lhop1  26064  aaliou3lem2  26395  ulmclm  26438  ulmss  26448  abelth  26492  cosord  26584  efif1olem4  26598  argimgt0  26665  logdivlt  26674  cxploglim  27030  dvdssqf  27190  mumullem1  27231  mumullem2  27232  bposlem6  27341  lgsdchr  27407  gausslemma2dlem1a  27417  m1lgs  27440  chtppilim  27527  lestr  27814  lestric  27820  madebdayim  27969  madebdaylemold  27979  ltslpss  27989  om2noseqf1o  28382  zsoring  28490  bdaypw2n0bndlem  28544  bdayfin  28568  ax5seg  29096  axpasch  29099  axlowdimlem16  29115  axeuclid  29121  axcontlem4  29125  usgr1v0e  29484  nb3gr2nb  29542  cplgr1v  29588  finsumvtxdg2size  29708  usgr2pthlem  29920  clwwlknwwlksn  30197  erclwwlknsym  30229  erclwwlkntr  30230  frgr3vlem1  30432  3vfriswmgrlem  30436  numclwwlk5  30547  minvecolem5  31041  ocsh  31443  shless  31519  leopadd  32292  leopmuli  32293  leopmul2i  32295  leoptr  32297  spansncv2  32453  mdsl0  32470  ssdmd1  32473  cvdmd  32497  cdj3i  32601  uzssico  32947  expgt0b  32980  eqgvscpbl  33497  qusvscpbl  33498  cmpcref  34108  acycgrsubgr  35469  cvmliftmolem1  35592  satffunlem2lem2  35717  mrsubff1  35825  msubff1  35867  lediv2aALT  35988  cgr3tr4  36363  colinearxfr  36386  lineext  36387  brsegle  36419  seglecgr12im  36421  segletr  36425  colinbtwnle  36429  outsideoftr  36440  lineelsb2  36459  ivthALT  36656  tailfb  36698  poimirlem29  38109  itg2addnclem  38131  itg2addnclem3  38133  itg2addnc  38134  incsequz  38208  mettrifi  38217  ismtycnv  38262  bfplem1  38282  ghomco  38351  rngoisocnv  38441  keridl  38492  dmncan1  38536  ax12indalem  39530  ax12inda2ALT  39531  omllaw4  39831  cmtcomlemN  39833  cvlexch2  39914  cvlatexch2  39922  cvrexch  40005  atexchltN  40026  3atlem5  40072  lplnribN  40136  linepsubN  40337  paddss1  40402  paddss2  40403  pmapjoin  40437  pmapjat1  40438  cdleme36a  41045  dib2dim  41828  dih2dimbALTN  41830  djhcvat42  42000  dihjatcclem4  42006  dihjat1lem  42013  lcfrlem6  42132  hlhillcs  42543  oexpreposd  42892  mulgt0b1d  43055  mullt0b1d  43066  pell1234qrmulcl  43393  pell14qrss1234  43394  pell14qrmulcl  43401  pell14qrreccl  43402  pell1qrss14  43406  monotoddzzfi  43480  oddcomabszz  43482  omabs2  43870  omcl3g  43872  tfsconcat0b  43884  naddwordnexlem4  43939  climinf  46143  2ffzoeq  47883  iccpartgt  47994  pgnbgreunbgrlem1  48696  pgnbgreunbgrlem4  48702  upwlkwlk  48722  uspgrsprf1  48730  rrx2xpref1o  49301  itschlc0yqe  49343  resipos  49557