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

Theorem 3imtr4d 260
Description: More general version of 3imtr4i 258. Useful for converting conditional definitions in a formula. (Contributed by NM, 26-Oct-1995.)
Hypotheses
Ref Expression
3imtr4d.1  |-  ( ph  ->  ( ps  ->  ch ) )
3imtr4d.2  |-  ( ph  ->  ( th  <->  ps )
)
3imtr4d.3  |-  ( ph  ->  ( ta  <->  ch )
)
Assertion
Ref Expression
3imtr4d  |-  ( ph  ->  ( th  ->  ta ) )

Proof of Theorem 3imtr4d
StepHypRef Expression
1 3imtr4d.2 . 2  |-  ( ph  ->  ( th  <->  ps )
)
2 3imtr4d.1 . . 3  |-  ( ph  ->  ( ps  ->  ch ) )
3 3imtr4d.3 . . 3  |-  ( ph  ->  ( ta  <->  ch )
)
42, 3sylibrd 226 . 2  |-  ( ph  ->  ( ps  ->  ta ) )
51, 4sylbid 207 1  |-  ( ph  ->  ( th  ->  ta ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177
This theorem is referenced by:  ax11indalem  2251  ax11inda2ALT  2252  unielrel  5357  fconst5  5912  soisores  6010  ovmpt2s  6160  caofrss  6300  caoftrn  6302  f1o2ndf1  6417  oaord  6753  omord2  6773  omcan  6775  oeord  6794  oecan  6795  nnaord  6825  nnmord  6838  omsmo  6860  ovec  6977  pmss12g  7003  cantnf  7609  pm54.43  7847  ttukeylem2  8350  axlttrn  9108  axltadd  9109  axmulgt0  9110  axsup  9111  ltadd2  9137  ltord1  9513  recex  9614  prodge0  9817  ltmul1  9820  lt2msq  9854  nnge1  9986  zltp1le  10285  uzss  10466  eluzp1m1  10469  ixxssixx  10890  zesq  11461  climrlim2  12300  rlimres  12311  climshftlem  12327  lo1add  12379  lo1mul  12380  rlimsqzlem  12401  lo1le  12404  isercolllem2  12418  isercoll  12420  climsup  12422  cvgcmp  12554  climcndslem1  12588  dvds1lem  12820  algcvg  13026  eucalgcvga  13036  rpexp12i  13081  crt  13126  pc2dvds  13211  pcmpt  13220  prmpwdvds  13231  1arith  13254  vdwlem2  13309  vdwlem6  13313  vdwlem8  13315  ercpbl  13733  ipopos  14545  subginv  14910  symggrp  15062  lsmless1x  15237  lsmless2x  15238  dprdss  15546  dvdsunit  15727  irredrmul  15771  isdrngd  15819  lspextmo  16091  domnchr  16772  zntoslem  16796  tgss  16992  neips  17136  opnnei  17143  lpss3  17167  ssrest  17198  t1t0  17370  kgen2ss  17544  isfild  17847  fgss  17862  fgss2  17863  cnpflf2  17989  fclsss1  18011  fclsss2  18012  tgpt0  18105  tsmsxp  18141  prdsxmslem2  18516  ngptgp  18634  nghmcn  18736  qdensere  18761  evth  18941  nmhmcn  19085  tchcph  19151  caussi  19207  equivcfil  19209  ivthlem2  19306  ovollb2lem  19341  ovolunlem1  19350  volun  19396  ioombl1lem4  19412  volsup2  19454  volcn  19455  ismbf3d  19503  itg2mulclem  19595  cpnord  19778  lhop1  19855  evlseu  19894  aaliou3lem2  20217  ulmclm  20260  ulmss  20270  abelth  20314  cosord  20391  efif1olem4  20404  argimgt0  20464  logdivlt  20473  cxploglim  20773  dvdssqf  20878  mumullem1  20919  mumullem2  20920  bposlem6  21030  lgsdchr  21089  m1lgs  21103  chtppilim  21126  nb3gra2nb  21421  spthispth  21530  wlkdvspth  21565  cycliscrct  21574  3v3e3cycl1  21588  4cycl4v4e  21610  4cycl4dv4e  21612  cusconngra  21620  eupatrl  21647  minvecolem5  22340  ocsh  22742  shless  22818  leopadd  23592  leopmuli  23593  leopmul2i  23595  leoptr  23597  spansncv2  23753  mdsl0  23770  ssdmd1  23773  cvdmd  23797  cdj3i  23901  cvmliftmolem1  24925  lediv2aALT  25074  relexp0  25086  predpo  25402  nodenselem5  25557  ax5seg  25785  axpasch  25788  axlowdimlem16  25804  axeuclid  25810  axcontlem4  25814  cgr3tr4  25894  colinearxfr  25917  lineext  25918  brsegle  25950  seglecgr12im  25952  segletr  25956  colinbtwnle  25960  outsideoftr  25971  lineelsb2  25990  itg2addnclem  26159  itg2addnclem3  26161  itg2addnc  26162  ivthALT  26232  tailfb  26300  incsequz  26346  mettrifi  26357  ismtycnv  26405  bfplem1  26425  ghomco  26452  rngoisocnv  26491  keridl  26536  dmncan1  26580  pell1234qrmulcl  26812  pell14qrss1234  26813  pell14qrmulcl  26820  pell14qrreccl  26821  pell1qrss14  26825  monotoddzzfi  26899  oddcomabszz  26901  f1otrspeq  27262  climinf  27603  swrdccatin12lem4  28029  swrdccatin12  28030  usgra2pthlem1  28044  frgra3vlem1  28108  3vfriswmgralem  28112  frgrawopreglem2  28152  usg2spot2nb  28172  2spotmdisj  28175  omllaw4  29733  cmtcomlemN  29735  cvlexch2  29816  cvlatexch2  29824  cvrexch  29906  atexchltN  29927  3atlem5  29973  lplnribN  30037  linepsubN  30238  paddss1  30303  paddss2  30304  pmapjoin  30338  pmapjat1  30339  cdleme36a  30946  dib2dim  31730  dih2dimbALTN  31732  djhcvat42  31902  dihjatcclem4  31908  dihjat1lem  31915  lcfrlem6  32034  hlhillcs  32448
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178
  Copyright terms: Public domain W3C validator