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  4683  unielrel  6247  predtrss  6295  fvrnressn  7133  fconst5  7180  soisores  7302  caofrss  7692  caoftrn  7694  f1o2ndf1  8101  oaord  8511  omord2  8531  omcan  8533  oeord  8552  oecan  8553  nnaord  8583  nnmord  8596  omsmo  8622  pmss12g  8842  cantnf  9646  pm54.43  9954  ttukeylem2  10463  axlttrn  11246  axltadd  11247  axmulgt0  11248  axsup  11249  ltadd2  11278  ltord1  11704  recex  11810  ltmul1  12032  lt2msq  12068  nnge1  12214  zltp1le  12583  uzss  12816  eluzp1m1  12819  prodge0rd  13060  ixxssixx  13320  zesq  14191  pfxccatin12lem3  14697  swrdccat3blem  14704  relexpsucnnr  14991  climrlim2  15513  rlimres  15524  climshftlem  15540  lo1add  15593  lo1mul  15594  rlimsqzlem  15615  lo1le  15618  isercolllem2  15632  isercoll  15634  climsup  15636  cvgcmp  15782  climcndslem1  15815  dvds1lem  16237  sumodd  16358  rprpwr  16529  algcvg  16546  eucalgcvga  16556  rpexp12i  16694  crth  16748  pc2dvds  16850  pcmpt  16863  prmpwdvds  16875  1arith  16898  vdwlem2  16953  vdwlem6  16957  vdwlem8  16959  ercpbl  17512  initoid  17963  termoid  17964  ipopos  18495  insubm  18745  subginv  19065  symggrp  19330  f1otrspeq  19377  lsmless1x  19574  lsmless2x  19575  dprdss  19961  rngpropd  20083  dvdsunit  20288  irredrmul  20336  isdrngd  20674  isdrngdOLD  20676  lspextmo  20963  rngqiprngimf1lem  21204  domnchr  21442  zntoslem  21466  evlseu  21990  mat2pmatf1  22616  tgss  22855  neips  23000  opnnei  23007  lpss3  23031  ssrest  23063  t1t0  23235  kgen2ss  23442  isfild  23745  fgss  23760  fgss2  23761  cnpflf2  23887  fclsss1  23909  fclsss2  23910  tgpt0  24006  tsmsxp  24042  prdsxmslem2  24417  ngptgp  24524  nghmcn  24633  qdensere  24657  evth  24858  nmhmcn  25020  tcphcph  25137  caussi  25197  equivcfil  25199  rrxmvallem  25304  ivthlem2  25353  ovollb2lem  25389  ovolunlem1  25398  volun  25446  ioombl1lem4  25462  volsup2  25506  volcn  25507  ismbf3d  25555  itg2mulclem  25647  cpnord  25837  lhop1  25919  aaliou3lem2  26251  ulmclm  26296  ulmss  26306  abelth  26351  cosord  26440  efif1olem4  26454  argimgt0  26521  logdivlt  26530  cxploglim  26888  dvdssqf  27048  mumullem1  27089  mumullem2  27090  bposlem6  27200  lgsdchr  27266  gausslemma2dlem1a  27276  m1lgs  27299  chtppilim  27386  sletr  27670  sletric  27676  madebdayim  27799  madebdaylemold  27809  sltlpss  27819  om2noseqf1o  28195  ax5seg  28865  axpasch  28868  axlowdimlem16  28884  axeuclid  28890  axcontlem4  28894  usgr1v0e  29253  nb3gr2nb  29311  cplgr1v  29357  finsumvtxdg2size  29478  usgr2pthlem  29693  clwwlknwwlksn  29967  erclwwlknsym  29999  erclwwlkntr  30000  frgr3vlem1  30202  3vfriswmgrlem  30206  numclwwlk5  30317  minvecolem5  30810  ocsh  31212  shless  31288  leopadd  32061  leopmuli  32062  leopmul2i  32064  leoptr  32066  spansncv2  32222  mdsl0  32239  ssdmd1  32242  cvdmd  32266  cdj3i  32370  uzssico  32707  expgt0b  32741  eqgvscpbl  33321  qusvscpbl  33322  cmpcref  33840  acycgrsubgr  35145  cvmliftmolem1  35268  satffunlem2lem2  35393  mrsubff1  35501  msubff1  35543  lediv2aALT  35664  cgr3tr4  36040  colinearxfr  36063  lineext  36064  brsegle  36096  seglecgr12im  36098  segletr  36102  colinbtwnle  36106  outsideoftr  36117  lineelsb2  36136  ivthALT  36323  tailfb  36365  poimirlem29  37643  itg2addnclem  37665  itg2addnclem3  37667  itg2addnc  37668  incsequz  37742  mettrifi  37751  ismtycnv  37796  bfplem1  37816  ghomco  37885  rngoisocnv  37975  keridl  38026  dmncan1  38070  ax12indalem  38938  ax12inda2ALT  38939  omllaw4  39239  cmtcomlemN  39241  cvlexch2  39322  cvlatexch2  39330  cvrexch  39414  atexchltN  39435  3atlem5  39481  lplnribN  39545  linepsubN  39746  paddss1  39811  paddss2  39812  pmapjoin  39846  pmapjat1  39847  cdleme36a  40454  dib2dim  41237  dih2dimbALTN  41239  djhcvat42  41409  dihjatcclem4  41415  dihjat1lem  41422  lcfrlem6  41541  hlhillcs  41952  oexpreposd  42310  mulgt0b1d  42460  mullt0b1d  42471  pell1234qrmulcl  42843  pell14qrss1234  42844  pell14qrmulcl  42851  pell14qrreccl  42852  pell1qrss14  42856  monotoddzzfi  42931  oddcomabszz  42933  omabs2  43321  omcl3g  43323  tfsconcat0b  43335  naddwordnexlem4  43390  climinf  45604  2ffzoeq  47328  iccpartgt  47428  pgnbgreunbgrlem1  48103  pgnbgreunbgrlem4  48109  upwlkwlk  48127  uspgrsprf1  48135  rrx2xpref1o  48707  itschlc0yqe  48749  resipos  48963