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

Theorem 3imtr4d 272
Description: More general version of 3imtr4i 270. 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 238 . 2  |-  ( ph  ->  ( ps  ->  ta ) )
51, 4sylbid 219 1  |-  ( ph  ->  ( th  ->  ta ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 188
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 189
This theorem is referenced by:  unielrel  5377  predpo  5415  fvrnressn  6092  fconst5  6135  soisores  6231  caofrss  6576  caoftrn  6578  f1o2ndf1  6913  oaord  7254  omord2  7274  omcan  7276  oeord  7295  oecan  7296  nnaord  7326  nnmord  7339  omsmo  7361  pmss12g  7504  cantnf  8201  pm54.43  8437  ttukeylem2  8942  axlttrn  9708  axltadd  9709  axmulgt0  9710  axsup  9711  ltadd2  9740  ltord1  10142  recex  10246  prodge0  10454  ltmul1  10457  lt2msq  10493  nnge1  10637  zltp1le  10988  uzss  11181  eluzp1m1  11184  ixxssixx  11651  zesq  12396  swrdccatin12lem3  12842  swrdccat3blem  12847  relexpsucnnr  13082  climrlim2  13604  rlimres  13615  climshftlem  13631  lo1add  13683  lo1mul  13684  rlimsqzlem  13705  lo1le  13708  isercolllem2  13722  isercoll  13724  climsup  13726  cvgcmp  13869  climcndslem1  13900  dvds1lem  14307  algcvg  14528  eucalgcvga  14538  rpexp12i  14667  crt  14719  pc2dvds  14821  pcmpt  14830  prmpwdvds  14841  1arith  14864  vdwlem2  14925  vdwlem6  14929  vdwlem8  14931  ercpbl  15448  initoid  15893  termoid  15894  ipopos  16399  subginv  16817  symggrp  17034  f1otrspeq  17081  lsmless1x  17289  lsmless2x  17290  dprdss  17655  dvdsunit  17884  irredrmul  17928  isdrngd  17993  lspextmo  18272  evlseu  18732  domnchr  19095  zntoslem  19119  mat2pmatf1  19745  tgss  19976  neips  20121  opnnei  20128  lpss3  20152  ssrest  20184  t1t0  20356  kgen2ss  20562  isfild  20865  fgss  20880  fgss2  20881  cnpflf2  21007  fclsss1  21029  fclsss2  21030  tgpt0  21125  tsmsxp  21161  prdsxmslem2  21536  ngptgp  21636  nghmcn  21758  qdensere  21782  evth  21979  nmhmcn  22126  tchcph  22203  caussi  22259  equivcfil  22261  rrxmvallem  22350  ivthlem2  22395  ovollb2lem  22433  ovolunlem1  22442  volun  22490  ioombl1lem4  22506  volsup2  22555  volcn  22556  ismbf3d  22602  itg2mulclem  22696  cpnord  22881  lhop1  22958  aaliou3lem2  23291  ulmclm  23334  ulmss  23344  abelth  23388  cosord  23473  efif1olem4  23486  argimgt0  23553  logdivlt  23562  cxploglim  23895  dvdssqf  24057  mumullem1  24098  mumullem2  24099  bposlem6  24209  lgsdchr  24268  m1lgs  24282  chtppilim  24305  ax5seg  24960  axpasch  24963  axlowdimlem16  24979  axeuclid  24985  axcontlem4  24989  elusuhgra  25087  nb3gra2nb  25175  spthispth  25295  wlkdvspth  25330  cycliscrct  25350  3v3e3cycl1  25364  4cycl4v4e  25386  4cycl4dv4e  25388  cusconngra  25396  erclwwlknsym  25546  erclwwlkntr  25547  clwlkfclwwlk  25564  eupatrl  25688  frgra3vlem1  25720  3vfriswmgralem  25724  frgrawopreglem2  25765  usg2spot2nb  25785  2spotmdisj  25788  numclwwlk5  25832  minvecolem5  26515  minvecolem5OLD  26525  ocsh  26928  shless  27004  leopadd  27777  leopmuli  27778  leopmul2i  27780  leoptr  27782  spansncv2  27938  mdsl0  27955  ssdmd1  27958  cvdmd  27982  cdj3i  28086  cmpcref  28679  cvmliftmolem1  30006  mrsubff1  30154  msubff1  30196  lediv2aALT  30323  nodenselem5  30573  cgr3tr4  30818  colinearxfr  30841  lineext  30842  brsegle  30874  seglecgr12im  30876  segletr  30880  colinbtwnle  30884  outsideoftr  30895  lineelsb2  30914  ivthALT  30990  tailfb  31032  poimirlem29  31889  itg2addnclem  31913  itg2addnclem3  31915  itg2addnc  31916  incsequz  31997  mettrifi  32006  ismtycnv  32054  bfplem1  32074  ghomco  32101  rngoisocnv  32140  keridl  32185  dmncan1  32229  ax12indalem  32441  ax12inda2ALT  32442  omllaw4  32737  cmtcomlemN  32739  cvlexch2  32820  cvlatexch2  32828  cvrexch  32910  atexchltN  32931  3atlem5  32977  lplnribN  33041  linepsubN  33242  paddss1  33307  paddss2  33308  pmapjoin  33342  pmapjat1  33343  cdleme36a  33952  dib2dim  34736  dih2dimbALTN  34738  djhcvat42  34908  dihjatcclem4  34914  dihjat1lem  34921  lcfrlem6  35040  hlhillcs  35454  pell1234qrmulcl  35627  pell14qrss1234  35628  pell14qrmulcl  35635  pell14qrreccl  35636  pell1qrss14  35640  monotoddzzfi  35716  oddcomabszz  35718  climinf  37510  climinfOLD  37511  iccpartgt  38459  2ffzoeq  38759  usgr1v0e  38960  usgra2pthlem1  38971  usgo0s0  39051  usgo0s0ALT  39052  usgo1s0ALT  39053  usgo1s0  39058  usgfis  39062
  Copyright terms: Public domain W3C validator