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  2268  ax12inda2ALT  2269  unielrel  5532  fvrnressn  6076  fconst5  6118  soisores  6211  caofrss  6557  caoftrn  6559  f1o2ndf1  6891  oaord  7196  omord2  7216  omcan  7218  oeord  7237  oecan  7238  nnaord  7268  nnmord  7281  omsmo  7303  pmss12g  7445  cantnf  8112  cantnfOLD  8134  pm54.43  8381  ttukeylem2  8890  axlttrn  9657  axltadd  9658  axmulgt0  9659  axsup  9660  ltadd2  9688  ltord1  10079  recex  10181  prodge0  10389  ltmul1  10392  lt2msq  10429  nnge1  10562  zltp1le  10912  uzss  11102  eluzp1m1  11105  ixxssixx  11543  zesq  12257  swrdccatin12lem3  12678  swrdccat3blem  12683  climrlim2  13333  rlimres  13344  climshftlem  13360  lo1add  13412  lo1mul  13413  rlimsqzlem  13434  lo1le  13437  isercolllem2  13451  isercoll  13453  climsup  13455  cvgcmp  13593  climcndslem1  13624  dvds1lem  13856  algcvg  14064  eucalgcvga  14074  rpexp12i  14122  crt  14167  pc2dvds  14261  pcmpt  14270  prmpwdvds  14281  1arith  14304  vdwlem2  14359  vdwlem6  14363  vdwlem8  14365  ercpbl  14804  ipopos  15647  subginv  16013  symggrp  16230  f1otrspeq  16278  lsmless1x  16470  lsmless2x  16471  dprdss  16878  dvdsunit  17113  irredrmul  17157  isdrngd  17221  lspextmo  17502  evlseu  17984  domnchr  18364  zntoslem  18390  mat2pmatf1  19025  tgss  19264  neips  19408  opnnei  19415  lpss3  19439  ssrest  19471  t1t0  19643  kgen2ss  19819  isfild  20122  fgss  20137  fgss2  20138  cnpflf2  20264  fclsss1  20286  fclsss2  20287  tgpt0  20380  tsmsxp  20420  prdsxmslem2  20795  ngptgp  20913  nghmcn  21015  qdensere  21040  evth  21222  nmhmcn  21366  tchcph  21443  caussi  21499  equivcfil  21501  ivthlem2  21627  ovollb2lem  21662  ovolunlem1  21671  volun  21718  ioombl1lem4  21734  volsup2  21777  volcn  21778  ismbf3d  21824  itg2mulclem  21916  cpnord  22101  lhop1  22178  aaliou3lem2  22501  ulmclm  22544  ulmss  22554  abelth  22598  cosord  22680  efif1olem4  22693  argimgt0  22753  logdivlt  22762  cxploglim  23063  dvdssqf  23168  mumullem1  23209  mumullem2  23210  bposlem6  23320  lgsdchr  23379  m1lgs  23393  chtppilim  23416  ax5seg  23945  axpasch  23948  axlowdimlem16  23964  axeuclid  23970  axcontlem4  23974  elusuhgra  24072  nb3gra2nb  24159  spthispth  24279  wlkdvspth  24314  cycliscrct  24334  3v3e3cycl1  24348  4cycl4v4e  24370  4cycl4dv4e  24372  cusconngra  24380  erclwwlknsym  24530  erclwwlkntr  24531  clwlkfclwwlk  24548  eupatrl  24672  frgra3vlem1  24704  3vfriswmgralem  24708  frgrawopreglem2  24750  usg2spot2nb  24770  2spotmdisj  24773  numclwwlk5  24817  minvecolem5  25501  ocsh  25905  shless  25981  leopadd  26755  leopmuli  26756  leopmul2i  26758  leoptr  26760  spansncv2  26916  mdsl0  26933  ssdmd1  26936  cvdmd  26960  cdj3i  27064  cvmliftmolem1  28394  lediv2aALT  28546  relexp0  28555  predpo  28869  nodenselem5  29050  cgr3tr4  29307  colinearxfr  29330  lineext  29331  brsegle  29363  seglecgr12im  29365  segletr  29369  colinbtwnle  29373  outsideoftr  29384  lineelsb2  29403  itg2addnclem  29671  itg2addnclem3  29673  itg2addnc  29674  ivthALT  29758  tailfb  29826  incsequz  29872  mettrifi  29881  ismtycnv  29929  bfplem1  29949  ghomco  29976  rngoisocnv  30015  keridl  30060  dmncan1  30104  pell1234qrmulcl  30423  pell14qrss1234  30424  pell14qrmulcl  30431  pell14qrreccl  30432  pell1qrss14  30436  monotoddzzfi  30510  oddcomabszz  30512  climinf  31176  2ffzoeq  31836  usgra2pthlem1  31848  usgo0s0  31930  usgo0s0ALT  31931  usgo1s0ALT  31932  usgo1s0  31937  usgfis  31941  omllaw4  34061  cmtcomlemN  34063  cvlexch2  34144  cvlatexch2  34152  cvrexch  34234  atexchltN  34255  3atlem5  34301  lplnribN  34365  linepsubN  34566  paddss1  34631  paddss2  34632  pmapjoin  34666  pmapjat1  34667  cdleme36a  35274  dib2dim  36058  dih2dimbALTN  36060  djhcvat42  36230  dihjatcclem4  36236  dihjat1lem  36243  lcfrlem6  36362  hlhillcs  36776
  Copyright terms: Public domain W3C validator