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  5821  predpo  5859  fvrnressn  6592  fconst5  6636  soisores  6741  caofrss  7096  caoftrn  7098  f1o2ndf1  7454  oaord  7798  omord2  7818  omcan  7820  oeord  7839  oecan  7840  nnaord  7870  nnmord  7883  omsmo  7905  pmss12g  8052  cantnf  8765  pm54.43  9036  ttukeylem2  9544  axlttrn  10322  axltadd  10323  axmulgt0  10324  axsup  10325  ltadd2  10353  ltord1  10766  recex  10871  prodge0  11082  ltmul1  11085  lt2msq  11120  nnge1  11258  zltp1le  11639  uzss  11920  eluzp1m1  11923  ixxssixx  12402  zesq  13201  swrdccatin12lem3  13710  swrdccat3blem  13715  relexpsucnnr  13984  climrlim2  14497  rlimres  14508  climshftlem  14524  lo1add  14576  lo1mul  14577  rlimsqzlem  14598  lo1le  14601  isercolllem2  14615  isercoll  14617  climsup  14619  cvgcmp  14767  climcndslem1  14800  dvds1lem  15215  sumodd  15333  algcvg  15511  eucalgcvga  15521  rpexp12i  15656  crth  15705  pc2dvds  15805  pcmpt  15818  prmpwdvds  15830  1arith  15853  vdwlem2  15908  vdwlem6  15912  vdwlem8  15914  ercpbl  16431  initoid  16876  termoid  16877  ipopos  17381  subginv  17822  symggrp  18040  f1otrspeq  18087  lsmless1x  18279  lsmless2x  18280  dprdss  18648  dvdsunit  18883  irredrmul  18927  isdrngd  18994  lspextmo  19278  evlseu  19738  domnchr  20102  zntoslem  20127  mat2pmatf1  20756  tgss  20994  neips  21139  opnnei  21146  lpss3  21170  ssrest  21202  t1t0  21374  kgen2ss  21580  isfild  21883  fgss  21898  fgss2  21899  cnpflf2  22025  fclsss1  22047  fclsss2  22048  tgpt0  22143  tsmsxp  22179  prdsxmslem2  22555  ngptgp  22661  nghmcn  22770  qdensere  22794  evth  22979  nmhmcn  23140  tchcph  23256  caussi  23315  equivcfil  23317  rrxmvallem  23407  ivthlem2  23441  ovollb2lem  23476  ovolunlem1  23485  volun  23533  ioombl1lem4  23549  volsup2  23593  volcn  23594  ismbf3d  23640  itg2mulclem  23732  cpnord  23917  lhop1  23996  aaliou3lem2  24317  ulmclm  24360  ulmss  24370  abelth  24414  cosord  24498  efif1olem4  24511  argimgt0  24578  logdivlt  24587  cxploglim  24924  dvdssqf  25084  mumullem1  25125  mumullem2  25126  bposlem6  25234  lgsdchr  25300  gausslemma2dlem1a  25310  m1lgs  25333  chtppilim  25384  ax5seg  26038  axpasch  26041  axlowdimlem16  26057  axeuclid  26063  axcontlem4  26067  usgr1v0e  26438  nb3gr2nb  26505  cplgr1v  26557  finsumvtxdg2size  26677  usgr2pthlem  26890  clwwlknwwlksn  27187  erclwwlknsym  27222  erclwwlkntr  27223  clwlksfclwwlkOLD  27237  frgr3vlem1  27448  3vfriswmgrlem  27452  numclwwlk5  27577  minvecolem5  28067  ocsh  28472  shless  28548  leopadd  29321  leopmuli  29322  leopmul2i  29324  leoptr  29326  spansncv2  29482  mdsl0  29499  ssdmd1  29502  cvdmd  29526  cdj3i  29630  uzssico  29876  cmpcref  30247  cvmliftmolem1  31591  mrsubff1  31739  msubff1  31781  lediv2aALT  31899  sletr  32210  cgr3tr4  32486  colinearxfr  32509  lineext  32510  brsegle  32542  seglecgr12im  32544  segletr  32548  colinbtwnle  32552  outsideoftr  32563  lineelsb2  32582  ivthALT  32657  tailfb  32699  poimirlem29  33769  itg2addnclem  33792  itg2addnclem3  33794  itg2addnc  33795  incsequz  33875  mettrifi  33884  ismtycnv  33932  bfplem1  33952  ghomco  34021  rngoisocnv  34111  keridl  34162  dmncan1  34206  ax12indalem  34752  ax12inda2ALT  34753  omllaw4  35054  cmtcomlemN  35056  cvlexch2  35137  cvlatexch2  35145  cvrexch  35227  atexchltN  35248  3atlem5  35294  lplnribN  35358  linepsubN  35559  paddss1  35624  paddss2  35625  pmapjoin  35659  pmapjat1  35660  cdleme36a  36268  dib2dim  37052  dih2dimbALTN  37054  djhcvat42  37224  dihjatcclem4  37230  dihjat1lem  37237  lcfrlem6  37356  hlhillcs  37770  pell1234qrmulcl  37939  pell14qrss1234  37940  pell14qrmulcl  37947  pell14qrreccl  37948  pell1qrss14  37952  monotoddzzfi  38027  oddcomabszz  38029  climinf  40359  2ffzoeq  41866  iccpartgt  41891  upwlkwlk  42248  uspgrsprf1  42283
  Copyright terms: Public domain W3C validator