MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  3imtr4d Structured version   Visualization version   GIF version

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
StepHypRef Expression
1 3imtr4d.2 . 2 (𝜑 → (𝜃𝜓))
2 3imtr4d.1 . . 3 (𝜑 → (𝜓𝜒))
3 3imtr4d.3 . . 3 (𝜑 → (𝜏𝜒))
42, 3sylibrd 259 . 2 (𝜑 → (𝜓𝜏))
51, 4sylbid 239 1 (𝜑 → (𝜃𝜏))
Colors of variables: wff setvar class
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  4681  unielrel  6227  predtrss  6277  fvrnressn  7108  fconst5  7156  soisores  7273  caofrss  7654  caoftrn  7656  f1o2ndf1  8055  oaord  8495  omord2  8515  omcan  8517  oeord  8536  oecan  8537  nnaord  8567  nnmord  8580  omsmo  8605  pmss12g  8810  cantnf  9634  pm54.43  9942  ttukeylem2  10451  axlttrn  11232  axltadd  11233  axmulgt0  11234  axsup  11235  ltadd2  11264  ltord1  11686  recex  11792  ltmul1  12010  lt2msq  12045  nnge1  12186  zltp1le  12558  uzss  12791  eluzp1m1  12794  prodge0rd  13027  ixxssixx  13284  zesq  14135  pfxccatin12lem3  14626  swrdccat3blem  14633  relexpsucnnr  14916  climrlim2  15435  rlimres  15446  climshftlem  15462  lo1add  15515  lo1mul  15516  rlimsqzlem  15539  lo1le  15542  isercolllem2  15556  isercoll  15558  climsup  15560  cvgcmp  15706  climcndslem1  15739  dvds1lem  16155  sumodd  16275  rprpwr  16444  algcvg  16457  eucalgcvga  16467  rpexp12i  16605  crth  16655  pc2dvds  16756  pcmpt  16769  prmpwdvds  16781  1arith  16804  vdwlem2  16859  vdwlem6  16863  vdwlem8  16865  ercpbl  17436  initoid  17892  termoid  17893  ipopos  18430  insubm  18634  subginv  18940  symggrp  19187  f1otrspeq  19234  lsmless1x  19431  lsmless2x  19432  dprdss  19813  dvdsunit  20097  irredrmul  20143  isdrngd  20226  isdrngdOLD  20228  lspextmo  20532  domnchr  20951  zntoslem  20979  evlseu  21509  mat2pmatf1  22094  tgss  22334  neips  22480  opnnei  22487  lpss3  22511  ssrest  22543  t1t0  22715  kgen2ss  22922  isfild  23225  fgss  23240  fgss2  23241  cnpflf2  23367  fclsss1  23389  fclsss2  23390  tgpt0  23486  tsmsxp  23522  prdsxmslem2  23901  ngptgp  24008  nghmcn  24125  qdensere  24149  evth  24338  nmhmcn  24499  tcphcph  24617  caussi  24677  equivcfil  24679  rrxmvallem  24784  ivthlem2  24832  ovollb2lem  24868  ovolunlem1  24877  volun  24925  ioombl1lem4  24941  volsup2  24985  volcn  24986  ismbf3d  25034  itg2mulclem  25127  cpnord  25315  lhop1  25394  aaliou3lem2  25719  ulmclm  25762  ulmss  25772  abelth  25816  cosord  25903  efif1olem4  25917  argimgt0  25983  logdivlt  25992  cxploglim  26343  dvdssqf  26503  mumullem1  26544  mumullem2  26545  bposlem6  26653  lgsdchr  26719  gausslemma2dlem1a  26729  m1lgs  26752  chtppilim  26839  sletr  27122  sletric  27128  madebdayim  27239  madebdaylemold  27249  sltlpss  27258  ax5seg  27929  axpasch  27932  axlowdimlem16  27948  axeuclid  27954  axcontlem4  27958  usgr1v0e  28316  nb3gr2nb  28374  cplgr1v  28420  finsumvtxdg2size  28540  usgr2pthlem  28753  clwwlknwwlksn  29024  erclwwlknsym  29056  erclwwlkntr  29057  frgr3vlem1  29259  3vfriswmgrlem  29263  numclwwlk5  29374  minvecolem5  29865  ocsh  30267  shless  30343  leopadd  31116  leopmuli  31117  leopmul2i  31119  leoptr  31121  spansncv2  31277  mdsl0  31294  ssdmd1  31297  cvdmd  31321  cdj3i  31425  uzssico  31734  eqgvscpbl  32189  qusvscpbl  32190  cmpcref  32488  acycgrsubgr  33809  cvmliftmolem1  33932  satffunlem2lem2  34057  mrsubff1  34165  msubff1  34207  lediv2aALT  34322  cgr3tr4  34683  colinearxfr  34706  lineext  34707  brsegle  34739  seglecgr12im  34741  segletr  34745  colinbtwnle  34749  outsideoftr  34760  lineelsb2  34779  ivthALT  34853  tailfb  34895  poimirlem29  36153  itg2addnclem  36175  itg2addnclem3  36177  itg2addnc  36178  incsequz  36253  mettrifi  36262  ismtycnv  36307  bfplem1  36327  ghomco  36396  rngoisocnv  36486  keridl  36537  dmncan1  36581  ax12indalem  37453  ax12inda2ALT  37454  omllaw4  37754  cmtcomlemN  37756  cvlexch2  37837  cvlatexch2  37845  cvrexch  37929  atexchltN  37950  3atlem5  37996  lplnribN  38060  linepsubN  38261  paddss1  38326  paddss2  38327  pmapjoin  38361  pmapjat1  38362  cdleme36a  38969  dib2dim  39752  dih2dimbALTN  39754  djhcvat42  39924  dihjatcclem4  39930  dihjat1lem  39937  lcfrlem6  40056  hlhillcs  40471  oexpreposd  40850  mulgt0b2d  40972  pell1234qrmulcl  41221  pell14qrss1234  41222  pell14qrmulcl  41229  pell14qrreccl  41230  pell1qrss14  41234  monotoddzzfi  41309  oddcomabszz  41311  omabs2  41710  omcl3g  41712  naddwordnexlem4  41761  climinf  43933  2ffzoeq  45646  iccpartgt  45705  upwlkwlk  46127  uspgrsprf1  46135  rrx2xpref1o  46890  itschlc0yqe  46932
  Copyright terms: Public domain W3C validator