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

Theorem 3imtr4d 259
Description: More general version of 3imtr4i 257. 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 225 . 2  |-  ( ph  ->  ( ps  ->  ta ) )
51, 4sylbid 206 1  |-  ( ph  ->  ( th  ->  ta ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176
This theorem is referenced by:  ax11indalem  2149  ax11inda2ALT  2150  unielrel  5213  fconst5  5747  soisores  5840  ovmpt2s  5987  caofrss  6126  caoftrn  6128  oaord  6561  omord2  6581  omcan  6583  oeord  6602  oecan  6603  nnaord  6633  nnmord  6646  omsmo  6668  ovec  6784  pmss12g  6810  cantnf  7411  pm54.43  7649  ttukeylem2  8153  axlttrn  8911  axltadd  8912  axmulgt0  8913  axsup  8914  ltadd2  8940  ltord1  9315  recex  9416  prodge0  9619  ltmul1  9622  lt2msq  9656  nnge1  9788  zltp1le  10083  uzss  10264  eluzp1m1  10267  ixxssixx  10686  zesq  11240  climrlim2  12037  rlimres  12048  climshftlem  12064  lo1add  12116  lo1mul  12117  rlimsqzlem  12138  lo1le  12141  isercolllem2  12155  isercoll  12157  climsup  12159  cvgcmp  12290  climcndslem1  12324  dvds1lem  12556  algcvg  12762  eucalgcvga  12772  rpexp12i  12817  crt  12862  pc2dvds  12947  pcmpt  12956  prmpwdvds  12967  1arith  12990  vdwlem2  13045  vdwlem6  13049  vdwlem8  13051  ercpbl  13467  ipopos  14279  subginv  14644  symggrp  14796  lsmless1x  14971  lsmless2x  14972  dprdss  15280  dvdsunit  15461  irredrmul  15505  isdrngd  15553  lspextmo  15829  domnchr  16502  zntoslem  16526  tgss  16722  neips  16866  opnnei  16873  lpss3  16892  ssrest  16923  t1t0  17092  kgen2ss  17266  isfild  17569  fgss  17584  fgss2  17585  cnpflf2  17711  fclsss1  17733  fclsss2  17734  tgpt0  17817  tsmsxp  17853  prdsxmslem2  18091  ngptgp  18168  nghmcn  18270  qdensere  18295  evth  18473  nmhmcn  18617  tchcph  18683  caussi  18739  equivcfil  18741  ivthlem2  18828  ovollb2lem  18863  ovolunlem1  18872  volun  18918  ioombl1lem4  18934  volsup2  18976  volcn  18977  ismbf3d  19025  itg2mulclem  19117  cpnord  19300  lhop1  19377  evlseu  19416  aaliou3lem2  19739  ulmclm  19782  ulmss  19790  abelth  19833  cosord  19910  efif1olem4  19923  argimgt0  19982  logdivlt  19988  cxploglim  20288  dvdssqf  20392  mumullem1  20433  mumullem2  20434  bposlem6  20544  lgsdchr  20603  m1lgs  20617  chtppilim  20640  minvecolem5  21476  ocsh  21878  shless  21954  leopadd  22728  leopmuli  22729  leopmul2i  22731  leoptr  22733  spansncv2  22889  mdsl0  22906  ssdmd1  22909  cvdmd  22933  cdj3i  23037  rabss3d  23152  esumpcvgval  23461  cvmliftmolem1  23827  lediv2aALT  24028  relexp0  24040  predpo  24255  nodenselem5  24410  ax5seg  24638  axpasch  24641  axlowdimlem16  24657  axeuclid  24663  axcontlem4  24667  cgr3tr4  24747  colinearxfr  24770  lineext  24771  brsegle  24803  seglecgr12im  24805  segletr  24809  colinbtwnle  24813  outsideoftr  24824  lineelsb2  24843  itg2addnclem  25003  itg2addnc  25005  iccss3  25237  oriso  25317  truni1  25608  islimrs3  25684  islimrs4  25685  lvsovso2  25730  icccon2  25803  icccon4  25805  bosser  26270  ivthALT  26361  tailfb  26429  incsequz  26561  lpss2  26571  mettrifi  26576  ismtycnv  26629  bfplem1  26649  ghomco  26676  rngoisocnv  26715  keridl  26760  dmncan1  26804  pell1234qrmulcl  27043  pell14qrss1234  27044  pell14qrmulcl  27051  pell14qrreccl  27052  pell1qrss14  27056  monotoddzzfi  27130  oddcomabszz  27132  f1otrspeq  27493  climinf  27835  nb3gra2nb  28291  spthispth  28359  wlkdvspth  28366  cycliscrct  28375  eupatrl  28385  3v3e3cycl1  28390  4cycl4v4e  28412  4cycl4dv4e  28414  frgra3vlem1  28424  3vfriswmgralem  28428  omllaw4  30058  cmtcomlemN  30060  cvlexch2  30141  cvlatexch2  30149  cvrexch  30231  atexchltN  30252  3atlem5  30298  lplnribN  30362  linepsubN  30563  paddss1  30628  paddss2  30629  pmapjoin  30663  pmapjat1  30664  cdleme36a  31271  dib2dim  32055  dih2dimbALTN  32057  djhcvat42  32227  dihjatcclem4  32233  dihjat1lem  32240  lcfrlem6  32359  hlhillcs  32773
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 177
  Copyright terms: Public domain W3C validator