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  2252  ax12inda2ALT  2253  unielrel  5359  fconst5  5932  soisores  6015  caofrss  6352  caoftrn  6354  f1o2ndf1  6679  oaord  6982  omord2  7002  omcan  7004  oeord  7023  oecan  7024  nnaord  7054  nnmord  7067  omsmo  7089  ovec  7206  pmss12g  7235  cantnf  7897  cantnfOLD  7919  pm54.43  8166  ttukeylem2  8675  axlttrn  9443  axltadd  9444  axmulgt0  9445  axsup  9446  ltadd2  9474  ltord1  9862  recex  9964  prodge0  10172  ltmul1  10175  lt2msq  10212  nnge1  10344  zltp1le  10690  uzss  10877  eluzp1m1  10880  ixxssixx  11310  zesq  11983  swrdccatin12lem3  12377  swrdccat3blem  12382  climrlim2  13021  rlimres  13032  climshftlem  13048  lo1add  13100  lo1mul  13101  rlimsqzlem  13122  lo1le  13125  isercolllem2  13139  isercoll  13141  climsup  13143  cvgcmp  13275  climcndslem1  13308  dvds1lem  13540  algcvg  13747  eucalgcvga  13757  rpexp12i  13804  crt  13849  pc2dvds  13941  pcmpt  13950  prmpwdvds  13961  1arith  13984  vdwlem2  14039  vdwlem6  14043  vdwlem8  14045  ercpbl  14483  ipopos  15326  subginv  15681  symggrp  15898  f1otrspeq  15946  lsmless1x  16136  lsmless2x  16137  dprdss  16516  dvdsunit  16745  irredrmul  16789  isdrngd  16837  lspextmo  17115  domnchr  17863  zntoslem  17889  tgss  18473  neips  18617  opnnei  18624  lpss3  18648  ssrest  18680  t1t0  18852  kgen2ss  19028  isfild  19331  fgss  19346  fgss2  19347  cnpflf2  19473  fclsss1  19495  fclsss2  19496  tgpt0  19589  tsmsxp  19629  prdsxmslem2  20004  ngptgp  20122  nghmcn  20224  qdensere  20249  evth  20431  nmhmcn  20575  tchcph  20652  caussi  20708  equivcfil  20710  ivthlem2  20836  ovollb2lem  20871  ovolunlem1  20880  volun  20926  ioombl1lem4  20942  volsup2  20985  volcn  20986  ismbf3d  21032  itg2mulclem  21124  cpnord  21309  lhop1  21386  evlseu  21426  aaliou3lem2  21752  ulmclm  21795  ulmss  21805  abelth  21849  cosord  21931  efif1olem4  21944  argimgt0  22004  logdivlt  22013  cxploglim  22314  dvdssqf  22419  mumullem1  22460  mumullem2  22461  bposlem6  22571  lgsdchr  22630  m1lgs  22644  chtppilim  22667  ax5seg  23103  axpasch  23106  axlowdimlem16  23122  axeuclid  23128  axcontlem4  23132  nb3gra2nb  23282  spthispth  23391  wlkdvspth  23426  cycliscrct  23435  3v3e3cycl1  23449  4cycl4v4e  23471  4cycl4dv4e  23473  cusconngra  23481  eupatrl  23508  minvecolem5  24201  ocsh  24605  shless  24681  leopadd  25455  leopmuli  25456  leopmul2i  25458  leoptr  25460  spansncv2  25616  mdsl0  25633  ssdmd1  25636  cvdmd  25660  cdj3i  25764  cvmliftmolem1  27084  lediv2aALT  27235  relexp0  27244  predpo  27558  nodenselem5  27739  cgr3tr4  27996  colinearxfr  28019  lineext  28020  brsegle  28052  seglecgr12im  28054  segletr  28058  colinbtwnle  28062  outsideoftr  28073  lineelsb2  28092  itg2addnclem  28352  itg2addnclem3  28354  itg2addnc  28355  ivthALT  28439  tailfb  28507  incsequz  28553  mettrifi  28562  ismtycnv  28610  bfplem1  28630  ghomco  28657  rngoisocnv  28696  keridl  28741  dmncan1  28785  pell1234qrmulcl  29105  pell14qrss1234  29106  pell14qrmulcl  29113  pell14qrreccl  29114  pell1qrss14  29118  monotoddzzfi  29192  oddcomabszz  29194  climinf  29688  fvelrnfvelrnressn  30060  2ffzoeq  30123  usgra2pthlem1  30209  erclwwlknsym  30409  erclwwlkntr  30410  clwlkfclwwlk  30426  frgra3vlem1  30501  3vfriswmgralem  30505  frgrawopreglem2  30547  usg2spot2nb  30567  2spotmdisj  30570  numclwwlk5  30614  omllaw4  32579  cmtcomlemN  32581  cvlexch2  32662  cvlatexch2  32670  cvrexch  32752  atexchltN  32773  3atlem5  32819  lplnribN  32883  linepsubN  33084  paddss1  33149  paddss2  33150  pmapjoin  33184  pmapjat1  33185  cdleme36a  33792  dib2dim  34576  dih2dimbALTN  34578  djhcvat42  34748  dihjatcclem4  34754  dihjat1lem  34761  lcfrlem6  34880  hlhillcs  35294
  Copyright terms: Public domain W3C validator