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

Theorem 3imtr4d 260
Description: More general version of 3imtr4i 258. 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 226 . 2  |-  ( ph  ->  ( ps  ->  ta ) )
51, 4sylbid 207 1  |-  ( ph  ->  ( th  ->  ta ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177
This theorem is referenced by:  ax11indalem  2274  ax11inda2ALT  2275  unielrel  5394  fconst5  5949  soisores  6047  ovmpt2s  6197  caofrss  6337  caoftrn  6339  f1o2ndf1  6454  oaord  6790  omord2  6810  omcan  6812  oeord  6831  oecan  6832  nnaord  6862  nnmord  6875  omsmo  6897  ovec  7014  pmss12g  7040  cantnf  7649  pm54.43  7887  ttukeylem2  8390  axlttrn  9148  axltadd  9149  axmulgt0  9150  axsup  9151  ltadd2  9177  ltord1  9553  recex  9654  prodge0  9857  ltmul1  9860  lt2msq  9894  nnge1  10026  zltp1le  10325  uzss  10506  eluzp1m1  10509  ixxssixx  10930  zesq  11502  climrlim2  12341  rlimres  12352  climshftlem  12368  lo1add  12420  lo1mul  12421  rlimsqzlem  12442  lo1le  12445  isercolllem2  12459  isercoll  12461  climsup  12463  cvgcmp  12595  climcndslem1  12629  dvds1lem  12861  algcvg  13067  eucalgcvga  13077  rpexp12i  13122  crt  13167  pc2dvds  13252  pcmpt  13261  prmpwdvds  13272  1arith  13295  vdwlem2  13350  vdwlem6  13354  vdwlem8  13356  ercpbl  13774  ipopos  14586  subginv  14951  symggrp  15103  lsmless1x  15278  lsmless2x  15279  dprdss  15587  dvdsunit  15768  irredrmul  15812  isdrngd  15860  lspextmo  16132  domnchr  16813  zntoslem  16837  tgss  17033  neips  17177  opnnei  17184  lpss3  17208  ssrest  17240  t1t0  17412  kgen2ss  17587  isfild  17890  fgss  17905  fgss2  17906  cnpflf2  18032  fclsss1  18054  fclsss2  18055  tgpt0  18148  tsmsxp  18184  prdsxmslem2  18559  ngptgp  18677  nghmcn  18779  qdensere  18804  evth  18984  nmhmcn  19128  tchcph  19194  caussi  19250  equivcfil  19252  ivthlem2  19349  ovollb2lem  19384  ovolunlem1  19393  volun  19439  ioombl1lem4  19455  volsup2  19497  volcn  19498  ismbf3d  19546  itg2mulclem  19638  cpnord  19821  lhop1  19898  evlseu  19937  aaliou3lem2  20260  ulmclm  20303  ulmss  20313  abelth  20357  cosord  20434  efif1olem4  20447  argimgt0  20507  logdivlt  20516  cxploglim  20816  dvdssqf  20921  mumullem1  20962  mumullem2  20963  bposlem6  21073  lgsdchr  21132  m1lgs  21146  chtppilim  21169  nb3gra2nb  21464  spthispth  21573  wlkdvspth  21608  cycliscrct  21617  3v3e3cycl1  21631  4cycl4v4e  21653  4cycl4dv4e  21655  cusconngra  21663  eupatrl  21690  minvecolem5  22383  ocsh  22785  shless  22861  leopadd  23635  leopmuli  23636  leopmul2i  23638  leoptr  23640  spansncv2  23796  mdsl0  23813  ssdmd1  23816  cvdmd  23840  cdj3i  23944  cvmliftmolem1  24968  lediv2aALT  25117  relexp0  25129  predpo  25459  nodenselem5  25640  ax5seg  25877  axpasch  25880  axlowdimlem16  25896  axeuclid  25902  axcontlem4  25906  cgr3tr4  25986  colinearxfr  26009  lineext  26010  brsegle  26042  seglecgr12im  26044  segletr  26048  colinbtwnle  26052  outsideoftr  26063  lineelsb2  26082  itg2addnclem  26256  itg2addnclem3  26258  itg2addnc  26259  ivthALT  26338  tailfb  26406  incsequz  26452  mettrifi  26463  ismtycnv  26511  bfplem1  26531  ghomco  26558  rngoisocnv  26597  keridl  26642  dmncan1  26686  pell1234qrmulcl  26918  pell14qrss1234  26919  pell14qrmulcl  26926  pell14qrreccl  26927  pell1qrss14  26931  monotoddzzfi  27005  oddcomabszz  27007  f1otrspeq  27367  climinf  27708  2ffzoeq  28140  swrdccatin12lem4  28213  swrdccat3blem  28218  cshweqdif2  28270  usgra2pthlem1  28310  frgra3vlem1  28390  3vfriswmgralem  28394  frgrawopreglem2  28434  usg2spot2nb  28454  2spotmdisj  28457  omllaw4  30044  cmtcomlemN  30046  cvlexch2  30127  cvlatexch2  30135  cvrexch  30217  atexchltN  30238  3atlem5  30284  lplnribN  30348  linepsubN  30549  paddss1  30614  paddss2  30615  pmapjoin  30649  pmapjat1  30650  cdleme36a  31257  dib2dim  32041  dih2dimbALTN  32043  djhcvat42  32213  dihjatcclem4  32219  dihjat1lem  32226  lcfrlem6  32345  hlhillcs  32759
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178
  Copyright terms: Public domain W3C validator