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

Theorem 3imtr4d 283
Description: More general version of 3imtr4i 281. 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 249 . 2 (𝜑 → (𝜓𝜏))
51, 4sylbid 230 1 (𝜑 → (𝜃𝜏))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196
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 197
This theorem is referenced by:  unielrel  5648  predpo  5686  fvrnressn  6413  fconst5  6456  soisores  6562  caofrss  6915  caoftrn  6917  f1o2ndf1  7270  oaord  7612  omord2  7632  omcan  7634  oeord  7653  oecan  7654  nnaord  7684  nnmord  7697  omsmo  7719  pmss12g  7869  cantnf  8575  pm54.43  8811  ttukeylem2  9317  axlttrn  10095  axltadd  10096  axmulgt0  10097  axsup  10098  ltadd2  10126  ltord1  10539  recex  10644  prodge0  10855  ltmul1  10858  lt2msq  10893  nnge1  11031  zltp1le  11412  uzss  11693  eluzp1m1  11696  ixxssixx  12174  zesq  12970  swrdccatin12lem3  13471  swrdccat3blem  13476  relexpsucnnr  13746  climrlim2  14259  rlimres  14270  climshftlem  14286  lo1add  14338  lo1mul  14339  rlimsqzlem  14360  lo1le  14363  isercolllem2  14377  isercoll  14379  climsup  14381  cvgcmp  14529  climcndslem1  14562  dvds1lem  14974  sumodd  15092  algcvg  15270  eucalgcvga  15280  rpexp12i  15415  crth  15464  pc2dvds  15564  pcmpt  15577  prmpwdvds  15589  1arith  15612  vdwlem2  15667  vdwlem6  15671  vdwlem8  15673  ercpbl  16190  initoid  16636  termoid  16637  ipopos  17141  subginv  17582  symggrp  17801  f1otrspeq  17848  lsmless1x  18040  lsmless2x  18041  dprdss  18409  dvdsunit  18644  irredrmul  18688  isdrngd  18753  lspextmo  19037  evlseu  19497  domnchr  19861  zntoslem  19886  mat2pmatf1  20515  tgss  20753  neips  20898  opnnei  20905  lpss3  20929  ssrest  20961  t1t0  21133  kgen2ss  21339  isfild  21643  fgss  21658  fgss2  21659  cnpflf2  21785  fclsss1  21807  fclsss2  21808  tgpt0  21903  tsmsxp  21939  prdsxmslem2  22315  ngptgp  22421  nghmcn  22530  qdensere  22554  evth  22739  nmhmcn  22901  tchcph  23017  caussi  23076  equivcfil  23078  rrxmvallem  23168  ivthlem2  23202  ovollb2lem  23237  ovolunlem1  23246  volun  23294  ioombl1lem4  23310  volsup2  23354  volcn  23355  ismbf3d  23402  itg2mulclem  23494  cpnord  23679  lhop1  23758  aaliou3lem2  24079  ulmclm  24122  ulmss  24132  abelth  24176  cosord  24259  efif1olem4  24272  argimgt0  24339  logdivlt  24348  cxploglim  24685  dvdssqf  24845  mumullem1  24886  mumullem2  24887  bposlem6  24995  lgsdchr  25061  gausslemma2dlem1a  25071  m1lgs  25094  chtppilim  25145  ax5seg  25799  axpasch  25802  axlowdimlem16  25818  axeuclid  25824  axcontlem4  25828  usgr1v0e  26199  nb3gr2nb  26267  cplgr1v  26307  finsumvtxdg2size  26427  usgr2pthlem  26640  erclwwlksnsym  26927  erclwwlksntr  26928  clwlksfclwwlk  26942  frgr3vlem1  27117  3vfriswmgrlem  27121  numclwwlk5  27216  minvecolem5  27707  ocsh  28112  shless  28188  leopadd  28961  leopmuli  28962  leopmul2i  28964  leoptr  28966  spansncv2  29122  mdsl0  29139  ssdmd1  29142  cvdmd  29166  cdj3i  29270  uzssico  29520  cmpcref  29891  cvmliftmolem1  31237  mrsubff1  31385  msubff1  31427  lediv2aALT  31545  sletr  31857  cgr3tr4  32134  colinearxfr  32157  lineext  32158  brsegle  32190  seglecgr12im  32192  segletr  32196  colinbtwnle  32200  outsideoftr  32211  lineelsb2  32230  ivthALT  32305  tailfb  32347  poimirlem29  33409  itg2addnclem  33432  itg2addnclem3  33434  itg2addnc  33435  incsequz  33515  mettrifi  33524  ismtycnv  33572  bfplem1  33592  ghomco  33661  rngoisocnv  33751  keridl  33802  dmncan1  33846  ax12indalem  34049  ax12inda2ALT  34050  omllaw4  34352  cmtcomlemN  34354  cvlexch2  34435  cvlatexch2  34443  cvrexch  34525  atexchltN  34546  3atlem5  34592  lplnribN  34656  linepsubN  34857  paddss1  34922  paddss2  34923  pmapjoin  34957  pmapjat1  34958  cdleme36a  35567  dib2dim  36351  dih2dimbALTN  36353  djhcvat42  36523  dihjatcclem4  36529  dihjat1lem  36536  lcfrlem6  36655  hlhillcs  37069  pell1234qrmulcl  37238  pell14qrss1234  37239  pell14qrmulcl  37246  pell14qrreccl  37247  pell1qrss14  37251  monotoddzzfi  37326  oddcomabszz  37328  climinf  39638  2ffzoeq  41101  iccpartgt  41127  upwlkwlk  41485  uspgrsprf1  41520
  Copyright terms: Public domain W3C validator