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

Theorem 3imtr4d 259
Description: More general version of 3imtr4i 257. 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 225 . 2  |-  ( ph  ->  ( ps  ->  ta ) )
51, 4sylbid 206 1  |-  ( ph  ->  ( th  ->  ta ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176
This theorem is referenced by:  ax11indalem  2136  ax11inda2ALT  2137  unielrel  5197  fconst5  5731  soisores  5824  ovmpt2s  5971  caofrss  6110  caoftrn  6112  oaord  6545  omord2  6565  omcan  6567  oeord  6586  oecan  6587  nnaord  6617  nnmord  6630  omsmo  6652  ovec  6768  pmss12g  6794  cantnf  7395  pm54.43  7633  ttukeylem2  8137  axlttrn  8895  axltadd  8896  axmulgt0  8897  axsup  8898  ltadd2  8924  ltord1  9299  recex  9400  prodge0  9603  ltmul1  9606  lt2msq  9640  nnge1  9772  zltp1le  10067  uzss  10248  eluzp1m1  10251  ixxssixx  10670  zesq  11224  climrlim2  12021  rlimres  12032  climshftlem  12048  lo1add  12100  lo1mul  12101  rlimsqzlem  12122  lo1le  12125  isercolllem2  12139  isercoll  12141  climsup  12143  cvgcmp  12274  climcndslem1  12308  dvds1lem  12540  algcvg  12746  eucalgcvga  12756  rpexp12i  12801  crt  12846  pc2dvds  12931  pcmpt  12940  prmpwdvds  12951  1arith  12974  vdwlem2  13029  vdwlem6  13033  vdwlem8  13035  ercpbl  13451  ipopos  14263  subginv  14628  symggrp  14780  lsmless1x  14955  lsmless2x  14956  dprdss  15264  dvdsunit  15445  irredrmul  15489  isdrngd  15537  lspextmo  15813  domnchr  16486  zntoslem  16510  tgss  16706  neips  16850  opnnei  16857  lpss3  16876  ssrest  16907  t1t0  17076  kgen2ss  17250  isfild  17553  fgss  17568  fgss2  17569  cnpflf2  17695  fclsss1  17717  fclsss2  17718  tgpt0  17801  tsmsxp  17837  prdsxmslem2  18075  ngptgp  18152  nghmcn  18254  qdensere  18279  evth  18457  nmhmcn  18601  tchcph  18667  caussi  18723  equivcfil  18725  ivthlem2  18812  ovollb2lem  18847  ovolunlem1  18856  volun  18902  ioombl1lem4  18918  volsup2  18960  volcn  18961  ismbf3d  19009  itg2mulclem  19101  cpnord  19284  lhop1  19361  evlseu  19400  aaliou3lem2  19723  ulmclm  19766  ulmss  19774  abelth  19817  cosord  19894  efif1olem4  19907  argimgt0  19966  logdivlt  19972  cxploglim  20272  dvdssqf  20376  mumullem1  20417  mumullem2  20418  bposlem6  20528  lgsdchr  20587  m1lgs  20601  chtppilim  20624  minvecolem5  21460  ocsh  21862  shless  21938  leopadd  22712  leopmuli  22713  leopmul2i  22715  leoptr  22717  spansncv2  22873  mdsl0  22890  ssdmd1  22893  cvdmd  22917  cdj3i  23021  rabss3d  23136  esumpcvgval  23446  cvmliftmolem1  23812  lediv2aALT  24013  relexp0  24025  predpo  24184  nodenselem5  24339  ax5seg  24566  axpasch  24569  axlowdimlem16  24585  axeuclid  24591  axcontlem4  24595  cgr3tr4  24675  colinearxfr  24698  lineext  24699  brsegle  24731  seglecgr12im  24733  segletr  24737  colinbtwnle  24741  outsideoftr  24752  lineelsb2  24771  iccss3  25134  oriso  25214  truni1  25505  islimrs3  25581  islimrs4  25582  lvsovso2  25627  icccon2  25700  icccon4  25702  bosser  26167  ivthALT  26258  tailfb  26326  incsequz  26458  lpss2  26468  mettrifi  26473  ismtycnv  26526  bfplem1  26546  ghomco  26573  rngoisocnv  26612  keridl  26657  dmncan1  26701  pell1234qrmulcl  26940  pell14qrss1234  26941  pell14qrmulcl  26948  pell14qrreccl  26949  pell1qrss14  26953  monotoddzzfi  27027  oddcomabszz  27029  f1otrspeq  27390  climinf  27732  frgra3vlem1  28178  3vfriswmgralem  28182  omllaw4  29436  cmtcomlemN  29438  cvlexch2  29519  cvlatexch2  29527  cvrexch  29609  atexchltN  29630  3atlem5  29676  lplnribN  29740  linepsubN  29941  paddss1  30006  paddss2  30007  pmapjoin  30041  pmapjat1  30042  cdleme36a  30649  dib2dim  31433  dih2dimbALTN  31435  djhcvat42  31605  dihjatcclem4  31611  dihjat1lem  31618  lcfrlem6  31737  hlhillcs  32151
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 177
  Copyright terms: Public domain W3C validator