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  5698  predpo  5736  fvrnressn  6468  fconst5  6512  soisores  6617  caofrss  6972  caoftrn  6974  f1o2ndf1  7330  oaord  7672  omord2  7692  omcan  7694  oeord  7713  oecan  7714  nnaord  7744  nnmord  7757  omsmo  7779  pmss12g  7926  cantnf  8628  pm54.43  8864  ttukeylem2  9370  axlttrn  10148  axltadd  10149  axmulgt0  10150  axsup  10151  ltadd2  10179  ltord1  10592  recex  10697  prodge0  10908  ltmul1  10911  lt2msq  10946  nnge1  11084  zltp1le  11465  uzss  11746  eluzp1m1  11749  ixxssixx  12227  zesq  13027  swrdccatin12lem3  13536  swrdccat3blem  13541  relexpsucnnr  13809  climrlim2  14322  rlimres  14333  climshftlem  14349  lo1add  14401  lo1mul  14402  rlimsqzlem  14423  lo1le  14426  isercolllem2  14440  isercoll  14442  climsup  14444  cvgcmp  14592  climcndslem1  14625  dvds1lem  15040  sumodd  15158  algcvg  15336  eucalgcvga  15346  rpexp12i  15481  crth  15530  pc2dvds  15630  pcmpt  15643  prmpwdvds  15655  1arith  15678  vdwlem2  15733  vdwlem6  15737  vdwlem8  15739  ercpbl  16256  initoid  16702  termoid  16703  ipopos  17207  subginv  17648  symggrp  17866  f1otrspeq  17913  lsmless1x  18105  lsmless2x  18106  dprdss  18474  dvdsunit  18709  irredrmul  18753  isdrngd  18820  lspextmo  19104  evlseu  19564  domnchr  19928  zntoslem  19953  mat2pmatf1  20582  tgss  20820  neips  20965  opnnei  20972  lpss3  20996  ssrest  21028  t1t0  21200  kgen2ss  21406  isfild  21709  fgss  21724  fgss2  21725  cnpflf2  21851  fclsss1  21873  fclsss2  21874  tgpt0  21969  tsmsxp  22005  prdsxmslem2  22381  ngptgp  22487  nghmcn  22596  qdensere  22620  evth  22805  nmhmcn  22966  tchcph  23082  caussi  23141  equivcfil  23143  rrxmvallem  23233  ivthlem2  23267  ovollb2lem  23302  ovolunlem1  23311  volun  23359  ioombl1lem4  23375  volsup2  23419  volcn  23420  ismbf3d  23466  itg2mulclem  23558  cpnord  23743  lhop1  23822  aaliou3lem2  24143  ulmclm  24186  ulmss  24196  abelth  24240  cosord  24323  efif1olem4  24336  argimgt0  24403  logdivlt  24412  cxploglim  24749  dvdssqf  24909  mumullem1  24950  mumullem2  24951  bposlem6  25059  lgsdchr  25125  gausslemma2dlem1a  25135  m1lgs  25158  chtppilim  25209  ax5seg  25863  axpasch  25866  axlowdimlem16  25882  axeuclid  25888  axcontlem4  25892  usgr1v0e  26263  nb3gr2nb  26330  cplgr1v  26382  finsumvtxdg2size  26502  usgr2pthlem  26715  clwwlknwwlksn  27000  erclwwlknsym  27034  erclwwlkntr  27035  clwlksfclwwlk  27049  frgr3vlem1  27253  3vfriswmgrlem  27257  numclwwlk5  27375  minvecolem5  27865  ocsh  28270  shless  28346  leopadd  29119  leopmuli  29120  leopmul2i  29122  leoptr  29124  spansncv2  29280  mdsl0  29297  ssdmd1  29300  cvdmd  29324  cdj3i  29428  uzssico  29674  cmpcref  30045  cvmliftmolem1  31389  mrsubff1  31537  msubff1  31579  lediv2aALT  31697  sletr  32008  cgr3tr4  32284  colinearxfr  32307  lineext  32308  brsegle  32340  seglecgr12im  32342  segletr  32346  colinbtwnle  32350  outsideoftr  32361  lineelsb2  32380  ivthALT  32455  tailfb  32497  poimirlem29  33568  itg2addnclem  33591  itg2addnclem3  33593  itg2addnc  33594  incsequz  33674  mettrifi  33683  ismtycnv  33731  bfplem1  33751  ghomco  33820  rngoisocnv  33910  keridl  33961  dmncan1  34005  ax12indalem  34549  ax12inda2ALT  34550  omllaw4  34851  cmtcomlemN  34853  cvlexch2  34934  cvlatexch2  34942  cvrexch  35024  atexchltN  35045  3atlem5  35091  lplnribN  35155  linepsubN  35356  paddss1  35421  paddss2  35422  pmapjoin  35456  pmapjat1  35457  cdleme36a  36065  dib2dim  36849  dih2dimbALTN  36851  djhcvat42  37021  dihjatcclem4  37027  dihjat1lem  37034  lcfrlem6  37153  hlhillcs  37567  pell1234qrmulcl  37736  pell14qrss1234  37737  pell14qrmulcl  37744  pell14qrreccl  37745  pell1qrss14  37749  monotoddzzfi  37824  oddcomabszz  37826  climinf  40156  2ffzoeq  41663  iccpartgt  41688  upwlkwlk  42045  uspgrsprf1  42080
  Copyright terms: Public domain W3C validator