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  2259  ax12inda2ALT  2260  unielrel  5518  fvrnressn  6067  fconst5  6109  soisores  6204  caofrss  6554  caoftrn  6556  f1o2ndf1  6889  oaord  7194  omord2  7214  omcan  7216  oeord  7235  oecan  7236  nnaord  7266  nnmord  7279  omsmo  7301  pmss12g  7443  cantnf  8110  cantnfOLD  8132  pm54.43  8379  ttukeylem2  8888  axlttrn  9655  axltadd  9656  axmulgt0  9657  axsup  9658  ltadd2  9686  ltord1  10080  recex  10182  prodge0  10390  ltmul1  10393  lt2msq  10430  nnge1  10563  zltp1le  10914  uzss  11105  eluzp1m1  11108  ixxssixx  11547  zesq  12263  swrdccatin12lem3  12689  swrdccat3blem  12694  climrlim2  13344  rlimres  13355  climshftlem  13371  lo1add  13423  lo1mul  13424  rlimsqzlem  13445  lo1le  13448  isercolllem2  13462  isercoll  13464  climsup  13466  cvgcmp  13604  climcndslem1  13635  dvds1lem  13867  algcvg  14077  eucalgcvga  14087  rpexp12i  14135  crt  14180  pc2dvds  14274  pcmpt  14283  prmpwdvds  14294  1arith  14317  vdwlem2  14372  vdwlem6  14376  vdwlem8  14378  ercpbl  14818  ipopos  15659  subginv  16077  symggrp  16294  f1otrspeq  16341  lsmless1x  16533  lsmless2x  16534  dprdss  16944  dvdsunit  17180  irredrmul  17224  isdrngd  17289  lspextmo  17570  evlseu  18053  domnchr  18436  zntoslem  18462  mat2pmatf1  19097  tgss  19336  neips  19480  opnnei  19487  lpss3  19511  ssrest  19543  t1t0  19715  kgen2ss  19922  isfild  20225  fgss  20240  fgss2  20241  cnpflf2  20367  fclsss1  20389  fclsss2  20390  tgpt0  20483  tsmsxp  20523  prdsxmslem2  20898  ngptgp  21016  nghmcn  21118  qdensere  21143  evth  21325  nmhmcn  21469  tchcph  21546  caussi  21602  equivcfil  21604  rrxmvallem  21697  ivthlem2  21730  ovollb2lem  21765  ovolunlem1  21774  volun  21821  ioombl1lem4  21837  volsup2  21880  volcn  21881  ismbf3d  21927  itg2mulclem  22019  cpnord  22204  lhop1  22281  aaliou3lem2  22604  ulmclm  22647  ulmss  22657  abelth  22701  cosord  22784  efif1olem4  22797  argimgt0  22862  logdivlt  22871  cxploglim  23172  dvdssqf  23277  mumullem1  23318  mumullem2  23319  bposlem6  23429  lgsdchr  23488  m1lgs  23502  chtppilim  23525  ax5seg  24106  axpasch  24109  axlowdimlem16  24125  axeuclid  24131  axcontlem4  24135  elusuhgra  24233  nb3gra2nb  24320  spthispth  24440  wlkdvspth  24475  cycliscrct  24495  3v3e3cycl1  24509  4cycl4v4e  24531  4cycl4dv4e  24533  cusconngra  24541  erclwwlknsym  24691  erclwwlkntr  24692  clwlkfclwwlk  24709  eupatrl  24833  frgra3vlem1  24865  3vfriswmgralem  24869  frgrawopreglem2  24910  usg2spot2nb  24930  2spotmdisj  24933  numclwwlk5  24977  minvecolem5  25662  ocsh  26066  shless  26142  leopadd  26916  leopmuli  26917  leopmul2i  26919  leoptr  26921  spansncv2  27077  mdsl0  27094  ssdmd1  27097  cvdmd  27121  cdj3i  27225  cmpcref  27719  cvmliftmolem1  28592  mrsubff1  28740  msubff1  28782  lediv2aALT  28909  relexp0  28918  predpo  29232  nodenselem5  29413  cgr3tr4  29670  colinearxfr  29693  lineext  29694  brsegle  29726  seglecgr12im  29728  segletr  29732  colinbtwnle  29736  outsideoftr  29747  lineelsb2  29766  itg2addnclem  30034  itg2addnclem3  30036  itg2addnc  30037  ivthALT  30121  tailfb  30163  incsequz  30209  mettrifi  30218  ismtycnv  30266  bfplem1  30286  ghomco  30313  rngoisocnv  30352  keridl  30397  dmncan1  30441  pell1234qrmulcl  30759  pell14qrss1234  30760  pell14qrmulcl  30767  pell14qrreccl  30768  pell1qrss14  30772  monotoddzzfi  30846  oddcomabszz  30848  climinf  31516  2ffzoeq  32175  usgra2pthlem1  32187  usgo0s0  32269  usgo0s0ALT  32270  usgo1s0ALT  32271  usgo1s0  32276  usgfis  32280  omllaw4  34673  cmtcomlemN  34675  cvlexch2  34756  cvlatexch2  34764  cvrexch  34846  atexchltN  34867  3atlem5  34913  lplnribN  34977  linepsubN  35178  paddss1  35243  paddss2  35244  pmapjoin  35278  pmapjat1  35279  cdleme36a  35888  dib2dim  36672  dih2dimbALTN  36674  djhcvat42  36844  dihjatcclem4  36850  dihjat1lem  36857  lcfrlem6  36976  hlhillcs  37390
  Copyright terms: Public domain W3C validator