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

Theorem 3imtr4d 276
Description: More general version of 3imtr4i 274. 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 242 . 2  |-  ( ph  ->  ( ps  ->  ta ) )
51, 4sylbid 223 1  |-  ( ph  ->  ( th  ->  ta ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 189
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 190
This theorem is referenced by:  unielrel  5378  predpo  5416  fvrnressn  6102  fconst5  6145  soisores  6242  caofrss  6590  caoftrn  6592  f1o2ndf1  6930  oaord  7273  omord2  7293  omcan  7295  oeord  7314  oecan  7315  nnaord  7345  nnmord  7358  omsmo  7380  pmss12g  7523  cantnf  8223  pm54.43  8459  ttukeylem2  8965  axlttrn  9731  axltadd  9732  axmulgt0  9733  axsup  9734  ltadd2  9763  ltord1  10167  recex  10271  prodge0  10479  ltmul1  10482  lt2msq  10518  nnge1  10662  zltp1le  11014  uzss  11207  eluzp1m1  11210  ixxssixx  11677  zesq  12426  swrdccatin12lem3  12882  swrdccat3blem  12887  relexpsucnnr  13136  climrlim2  13659  rlimres  13670  climshftlem  13686  lo1add  13738  lo1mul  13739  rlimsqzlem  13760  lo1le  13763  isercolllem2  13777  isercoll  13779  climsup  13781  cvgcmp  13924  climcndslem1  13955  dvds1lem  14362  algcvg  14583  eucalgcvga  14593  rpexp12i  14722  crt  14774  pc2dvds  14876  pcmpt  14885  prmpwdvds  14896  1arith  14919  vdwlem2  14980  vdwlem6  14984  vdwlem8  14986  ercpbl  15503  initoid  15948  termoid  15949  ipopos  16454  subginv  16872  symggrp  17089  f1otrspeq  17136  lsmless1x  17344  lsmless2x  17345  dprdss  17710  dvdsunit  17939  irredrmul  17983  isdrngd  18048  lspextmo  18327  evlseu  18787  domnchr  19151  zntoslem  19175  mat2pmatf1  19801  tgss  20032  neips  20177  opnnei  20184  lpss3  20208  ssrest  20240  t1t0  20412  kgen2ss  20618  isfild  20921  fgss  20936  fgss2  20937  cnpflf2  21063  fclsss1  21085  fclsss2  21086  tgpt0  21181  tsmsxp  21217  prdsxmslem2  21592  ngptgp  21692  nghmcn  21814  qdensere  21838  evth  22035  nmhmcn  22182  tchcph  22259  caussi  22315  equivcfil  22317  rrxmvallem  22406  ivthlem2  22451  ovollb2lem  22489  ovolunlem1  22498  volun  22546  ioombl1lem4  22562  volsup2  22611  volcn  22612  ismbf3d  22658  itg2mulclem  22752  cpnord  22937  lhop1  23014  aaliou3lem2  23347  ulmclm  23390  ulmss  23400  abelth  23444  cosord  23529  efif1olem4  23542  argimgt0  23609  logdivlt  23618  cxploglim  23951  dvdssqf  24113  mumullem1  24154  mumullem2  24155  bposlem6  24265  lgsdchr  24324  m1lgs  24338  chtppilim  24361  ax5seg  25016  axpasch  25019  axlowdimlem16  25035  axeuclid  25041  axcontlem4  25045  elusuhgra  25143  nb3gra2nb  25231  spthispth  25351  wlkdvspth  25386  cycliscrct  25406  3v3e3cycl1  25420  4cycl4v4e  25442  4cycl4dv4e  25444  cusconngra  25452  erclwwlknsym  25602  erclwwlkntr  25603  clwlkfclwwlk  25620  eupatrl  25744  frgra3vlem1  25776  3vfriswmgralem  25780  frgrawopreglem2  25821  usg2spot2nb  25841  2spotmdisj  25844  numclwwlk5  25888  minvecolem5  26571  minvecolem5OLD  26581  ocsh  26984  shless  27060  leopadd  27833  leopmuli  27834  leopmul2i  27836  leoptr  27838  spansncv2  27994  mdsl0  28011  ssdmd1  28014  cvdmd  28038  cdj3i  28142  cmpcref  28725  cvmliftmolem1  30052  mrsubff1  30200  msubff1  30242  lediv2aALT  30369  nodenselem5  30622  cgr3tr4  30867  colinearxfr  30890  lineext  30891  brsegle  30923  seglecgr12im  30925  segletr  30929  colinbtwnle  30933  outsideoftr  30944  lineelsb2  30963  ivthALT  31039  tailfb  31081  poimirlem29  32013  itg2addnclem  32037  itg2addnclem3  32039  itg2addnc  32040  incsequz  32121  mettrifi  32130  ismtycnv  32178  bfplem1  32198  ghomco  32225  rngoisocnv  32264  keridl  32309  dmncan1  32353  ax12indalem  32560  ax12inda2ALT  32561  omllaw4  32856  cmtcomlemN  32858  cvlexch2  32939  cvlatexch2  32947  cvrexch  33029  atexchltN  33050  3atlem5  33096  lplnribN  33160  linepsubN  33361  paddss1  33426  paddss2  33427  pmapjoin  33461  pmapjat1  33462  cdleme36a  34071  dib2dim  34855  dih2dimbALTN  34857  djhcvat42  35027  dihjatcclem4  35033  dihjat1lem  35040  lcfrlem6  35159  hlhillcs  35573  pell1234qrmulcl  35745  pell14qrss1234  35746  pell14qrmulcl  35753  pell14qrreccl  35754  pell1qrss14  35758  monotoddzzfi  35834  oddcomabszz  35836  climinf  37721  climinfOLD  37722  iccpartgt  38778  2ffzoeq  39105  usgr1v0e  39441  nb3gr2nb  39507  cplgr1v  39546  wlk1wlk  39698  sPthisPth  39759  cyclisCrct  39820  usgra2pthlem1  39939  usgo0s0  40019  usgo0s0ALT  40020  usgo1s0ALT  40021  usgo1s0  40026  usgfis  40030
  Copyright terms: Public domain W3C validator