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

Theorem 3imtr4d 268
Description: More general version of 3imtr4i 266. 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 234 . 2  |-  ( ph  ->  ( ps  ->  ta ) )
51, 4sylbid 215 1  |-  ( ph  ->  ( th  ->  ta ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184
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 185
This theorem is referenced by:  ax12indalem  2277  ax12inda2ALT  2278  unielrel  5515  fvrnressn  6062  fconst5  6105  soisores  6198  caofrss  6546  caoftrn  6548  f1o2ndf1  6881  oaord  7188  omord2  7208  omcan  7210  oeord  7229  oecan  7230  nnaord  7260  nnmord  7273  omsmo  7295  pmss12g  7438  cantnf  8103  cantnfOLD  8125  pm54.43  8372  ttukeylem2  8881  axlttrn  9646  axltadd  9647  axmulgt0  9648  axsup  9649  ltadd2  9677  ltord1  10075  recex  10177  prodge0  10385  ltmul1  10388  lt2msq  10424  nnge1  10557  zltp1le  10909  uzss  11102  eluzp1m1  11105  ixxssixx  11546  zesq  12271  swrdccatin12lem3  12706  swrdccat3blem  12711  relexpsucnnr  12942  climrlim2  13452  rlimres  13463  climshftlem  13479  lo1add  13531  lo1mul  13532  rlimsqzlem  13553  lo1le  13556  isercolllem2  13570  isercoll  13572  climsup  13574  cvgcmp  13712  climcndslem1  13743  dvds1lem  14079  algcvg  14289  eucalgcvga  14299  rpexp12i  14347  crt  14392  pc2dvds  14486  pcmpt  14495  prmpwdvds  14506  1arith  14529  vdwlem2  14584  vdwlem6  14588  vdwlem8  14590  ercpbl  15038  initoid  15483  termoid  15484  ipopos  15989  subginv  16407  symggrp  16624  f1otrspeq  16671  lsmless1x  16863  lsmless2x  16864  dprdss  17271  dvdsunit  17507  irredrmul  17551  isdrngd  17616  lspextmo  17897  evlseu  18380  domnchr  18744  zntoslem  18768  mat2pmatf1  19397  tgss  19637  neips  19781  opnnei  19788  lpss3  19812  ssrest  19844  t1t0  20016  kgen2ss  20222  isfild  20525  fgss  20540  fgss2  20541  cnpflf2  20667  fclsss1  20689  fclsss2  20690  tgpt0  20783  tsmsxp  20823  prdsxmslem2  21198  ngptgp  21316  nghmcn  21418  qdensere  21443  evth  21625  nmhmcn  21769  tchcph  21846  caussi  21902  equivcfil  21904  rrxmvallem  21997  ivthlem2  22030  ovollb2lem  22065  ovolunlem1  22074  volun  22121  ioombl1lem4  22137  volsup2  22180  volcn  22181  ismbf3d  22227  itg2mulclem  22319  cpnord  22504  lhop1  22581  aaliou3lem2  22905  ulmclm  22948  ulmss  22958  abelth  23002  cosord  23085  efif1olem4  23098  argimgt0  23165  logdivlt  23174  cxploglim  23505  dvdssqf  23610  mumullem1  23651  mumullem2  23652  bposlem6  23762  lgsdchr  23821  m1lgs  23835  chtppilim  23858  ax5seg  24443  axpasch  24446  axlowdimlem16  24462  axeuclid  24468  axcontlem4  24472  elusuhgra  24570  nb3gra2nb  24657  spthispth  24777  wlkdvspth  24812  cycliscrct  24832  3v3e3cycl1  24846  4cycl4v4e  24868  4cycl4dv4e  24870  cusconngra  24878  erclwwlknsym  25028  erclwwlkntr  25029  clwlkfclwwlk  25046  eupatrl  25170  frgra3vlem1  25202  3vfriswmgralem  25206  frgrawopreglem2  25247  usg2spot2nb  25267  2spotmdisj  25270  numclwwlk5  25314  minvecolem5  25995  ocsh  26399  shless  26475  leopadd  27249  leopmuli  27250  leopmul2i  27252  leoptr  27254  spansncv2  27410  mdsl0  27427  ssdmd1  27430  cvdmd  27454  cdj3i  27558  cmpcref  28088  cvmliftmolem1  28990  mrsubff1  29138  msubff1  29180  lediv2aALT  29307  predpo  29504  nodenselem5  29685  cgr3tr4  29930  colinearxfr  29953  lineext  29954  brsegle  29986  seglecgr12im  29988  segletr  29992  colinbtwnle  29996  outsideoftr  30007  lineelsb2  30026  itg2addnclem  30306  itg2addnclem3  30308  itg2addnc  30309  ivthALT  30393  tailfb  30435  incsequz  30481  mettrifi  30490  ismtycnv  30538  bfplem1  30558  ghomco  30585  rngoisocnv  30624  keridl  30669  dmncan1  30713  pell1234qrmulcl  31030  pell14qrss1234  31031  pell14qrmulcl  31038  pell14qrreccl  31039  pell1qrss14  31043  monotoddzzfi  31117  oddcomabszz  31119  climinf  31851  2ffzoeq  32715  usgra2pthlem1  32725  usgo0s0  32807  usgo0s0ALT  32808  usgo1s0ALT  32809  usgo1s0  32814  usgfis  32818  omllaw4  35368  cmtcomlemN  35370  cvlexch2  35451  cvlatexch2  35459  cvrexch  35541  atexchltN  35562  3atlem5  35608  lplnribN  35672  linepsubN  35873  paddss1  35938  paddss2  35939  pmapjoin  35973  pmapjat1  35974  cdleme36a  36583  dib2dim  37367  dih2dimbALTN  37369  djhcvat42  37539  dihjatcclem4  37545  dihjat1lem  37552  lcfrlem6  37671  hlhillcs  38085
  Copyright terms: Public domain W3C validator