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

Theorem 3imtr4d 295
Description: More general version of 3imtr4i 293. 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 260 . 2 (𝜑 → (𝜓𝜏))
51, 4sylbid 241 1 (𝜑 → (𝜃𝜏))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207
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 208
This theorem is referenced by:  rmosn  4654  unielrel  6123  predpo  6164  fvrnressn  6919  fconst5  6964  soisores  7072  caofrss  7432  caoftrn  7434  f1o2ndf1  7809  oaord  8163  omord2  8183  omcan  8185  oeord  8204  oecan  8205  nnaord  8235  nnmord  8248  omsmo  8271  pmss12g  8423  cantnf  9145  pm54.43  9418  ttukeylem2  9921  axlttrn  10702  axltadd  10703  axmulgt0  10704  axsup  10705  ltadd2  10733  ltord1  11155  recex  11261  ltmul1  11479  lt2msq  11514  nnge1  11654  zltp1le  12021  uzss  12254  eluzp1m1  12257  prodge0rd  12486  ixxssixx  12742  zesq  13577  pfxccatin12lem3  14084  swrdccat3blem  14091  relexpsucnnr  14374  climrlim2  14894  rlimres  14905  climshftlem  14921  lo1add  14973  lo1mul  14974  rlimsqzlem  14995  lo1le  14998  isercolllem2  15012  isercoll  15014  climsup  15016  cvgcmp  15161  climcndslem1  15194  dvds1lem  15611  sumodd  15729  algcvg  15910  eucalgcvga  15920  rpexp12i  16056  crth  16105  pc2dvds  16205  pcmpt  16218  prmpwdvds  16230  1arith  16253  vdwlem2  16308  vdwlem6  16312  vdwlem8  16314  ercpbl  16812  initoid  17255  termoid  17256  ipopos  17760  subginv  18216  symggrp  18448  f1otrspeq  18495  lsmless1x  18689  lsmless2x  18690  dprdss  19071  dvdsunit  19333  irredrmul  19377  isdrngd  19447  lspextmo  19748  evlseu  20214  domnchr  20595  zntoslem  20619  mat2pmatf1  21253  tgss  21492  neips  21637  opnnei  21644  lpss3  21668  ssrest  21700  t1t0  21872  kgen2ss  22079  isfild  22382  fgss  22397  fgss2  22398  cnpflf2  22524  fclsss1  22546  fclsss2  22547  tgpt0  22642  tsmsxp  22678  prdsxmslem2  23054  ngptgp  23160  nghmcn  23269  qdensere  23293  evth  23478  nmhmcn  23639  tcphcph  23755  caussi  23815  equivcfil  23817  rrxmvallem  23922  ivthlem2  23968  ovollb2lem  24004  ovolunlem1  24013  volun  24061  ioombl1lem4  24077  volsup2  24121  volcn  24122  ismbf3d  24170  itg2mulclem  24262  cpnord  24447  lhop1  24526  aaliou3lem2  24847  ulmclm  24890  ulmss  24900  abelth  24944  cosord  25029  efif1olem4  25042  argimgt0  25108  logdivlt  25117  cxploglim  25469  dvdssqf  25629  mumullem1  25670  mumullem2  25671  bposlem6  25779  lgsdchr  25845  gausslemma2dlem1a  25855  m1lgs  25878  chtppilim  25965  ax5seg  26638  axpasch  26641  axlowdimlem16  26657  axeuclid  26663  axcontlem4  26667  usgr1v0e  27022  nb3gr2nb  27080  cplgr1v  27126  finsumvtxdg2size  27246  usgr2pthlem  27458  clwwlknwwlksn  27730  erclwwlknsym  27763  erclwwlkntr  27764  frgr3vlem1  27966  3vfriswmgrlem  27970  numclwwlk5  28081  minvecolem5  28572  ocsh  28974  shless  29050  leopadd  29823  leopmuli  29824  leopmul2i  29826  leoptr  29828  spansncv2  29984  mdsl0  30001  ssdmd1  30004  cvdmd  30028  cdj3i  30132  uzssico  30420  eqgvscpbl  30833  qusvscpbl  30834  cmpcref  31000  acycgrsubgr  32289  cvmliftmolem1  32412  satffunlem2lem2  32537  mrsubff1  32645  msubff1  32687  lediv2aALT  32804  sletr  33121  cgr3tr4  33397  colinearxfr  33420  lineext  33421  brsegle  33453  seglecgr12im  33455  segletr  33459  colinbtwnle  33463  outsideoftr  33474  lineelsb2  33493  ivthALT  33567  tailfb  33609  poimirlem29  34788  itg2addnclem  34810  itg2addnclem3  34812  itg2addnc  34813  incsequz  34891  mettrifi  34900  ismtycnv  34948  bfplem1  34968  ghomco  35037  rngoisocnv  35127  keridl  35178  dmncan1  35222  ax12indalem  35948  ax12inda2ALT  35949  omllaw4  36249  cmtcomlemN  36251  cvlexch2  36332  cvlatexch2  36340  cvrexch  36423  atexchltN  36444  3atlem5  36490  lplnribN  36554  linepsubN  36755  paddss1  36820  paddss2  36821  pmapjoin  36855  pmapjat1  36856  cdleme36a  37463  dib2dim  38246  dih2dimbALTN  38248  djhcvat42  38418  dihjatcclem4  38424  dihjat1lem  38431  lcfrlem6  38550  hlhillcs  38961  oexpreposd  39044  pell1234qrmulcl  39317  pell14qrss1234  39318  pell14qrmulcl  39325  pell14qrreccl  39326  pell1qrss14  39330  monotoddzzfi  39404  oddcomabszz  39406  climinf  41752  2ffzoeq  43394  iccpartgt  43419  upwlkwlk  43846  uspgrsprf1  43854  rrx2xpref1o  44537  itschlc0yqe  44579
  Copyright terms: Public domain W3C validator