MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  3imtr4d 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  2233  ax11inda2ALT  2234  unielrel  5336  fconst5  5890  soisores  5988  ovmpt2s  6138  caofrss  6278  caoftrn  6280  oaord  6728  omord2  6748  omcan  6750  oeord  6769  oecan  6770  nnaord  6800  nnmord  6813  omsmo  6835  ovec  6952  pmss12g  6978  cantnf  7584  pm54.43  7822  ttukeylem2  8325  axlttrn  9083  axltadd  9084  axmulgt0  9085  axsup  9086  ltadd2  9112  ltord1  9487  recex  9588  prodge0  9791  ltmul1  9794  lt2msq  9828  nnge1  9960  zltp1le  10259  uzss  10440  eluzp1m1  10443  ixxssixx  10864  zesq  11431  climrlim2  12270  rlimres  12281  climshftlem  12297  lo1add  12349  lo1mul  12350  rlimsqzlem  12371  lo1le  12374  isercolllem2  12388  isercoll  12390  climsup  12392  cvgcmp  12524  climcndslem1  12558  dvds1lem  12790  algcvg  12996  eucalgcvga  13006  rpexp12i  13051  crt  13096  pc2dvds  13181  pcmpt  13190  prmpwdvds  13201  1arith  13224  vdwlem2  13279  vdwlem6  13283  vdwlem8  13285  ercpbl  13703  ipopos  14515  subginv  14880  symggrp  15032  lsmless1x  15207  lsmless2x  15208  dprdss  15516  dvdsunit  15697  irredrmul  15741  isdrngd  15789  lspextmo  16061  domnchr  16738  zntoslem  16762  tgss  16958  neips  17102  opnnei  17109  lpss3  17133  ssrest  17164  t1t0  17336  kgen2ss  17510  isfild  17813  fgss  17828  fgss2  17829  cnpflf2  17955  fclsss1  17977  fclsss2  17978  tgpt0  18071  tsmsxp  18107  prdsxmslem2  18451  ngptgp  18550  nghmcn  18652  qdensere  18677  evth  18857  nmhmcn  19001  tchcph  19067  caussi  19123  equivcfil  19125  ivthlem2  19218  ovollb2lem  19253  ovolunlem1  19262  volun  19308  ioombl1lem4  19324  volsup2  19366  volcn  19367  ismbf3d  19415  itg2mulclem  19507  cpnord  19690  lhop1  19767  evlseu  19806  aaliou3lem2  20129  ulmclm  20172  ulmss  20182  abelth  20226  cosord  20303  efif1olem4  20316  argimgt0  20376  logdivlt  20385  cxploglim  20685  dvdssqf  20790  mumullem1  20831  mumullem2  20832  bposlem6  20942  lgsdchr  21001  m1lgs  21015  chtppilim  21038  nb3gra2nb  21332  spthispth  21429  wlkdvspth  21458  cycliscrct  21467  3v3e3cycl1  21481  4cycl4v4e  21503  4cycl4dv4e  21505  cusconngra  21513  eupatrl  21540  minvecolem5  22233  ocsh  22635  shless  22711  leopadd  23485  leopmuli  23486  leopmul2i  23488  leoptr  23490  spansncv2  23646  mdsl0  23663  ssdmd1  23666  cvdmd  23690  cdj3i  23794  cvmliftmolem1  24749  lediv2aALT  24898  relexp0  24910  predpo  25210  nodenselem5  25365  ax5seg  25593  axpasch  25596  axlowdimlem16  25612  axeuclid  25618  axcontlem4  25622  cgr3tr4  25702  colinearxfr  25725  lineext  25726  brsegle  25758  seglecgr12im  25760  segletr  25764  colinbtwnle  25768  outsideoftr  25779  lineelsb2  25798  itg2addnclem  25959  itg2addnc  25961  ivthALT  26031  tailfb  26099  incsequz  26145  mettrifi  26156  ismtycnv  26204  bfplem1  26224  ghomco  26251  rngoisocnv  26290  keridl  26335  dmncan1  26379  pell1234qrmulcl  26611  pell14qrss1234  26612  pell14qrmulcl  26619  pell14qrreccl  26620  pell1qrss14  26624  monotoddzzfi  26698  oddcomabszz  26700  f1otrspeq  27061  climinf  27402  frgra3vlem1  27755  3vfriswmgralem  27759  frgrawopreglem2  27799  omllaw4  29363  cmtcomlemN  29365  cvlexch2  29446  cvlatexch2  29454  cvrexch  29536  atexchltN  29557  3atlem5  29603  lplnribN  29667  linepsubN  29868  paddss1  29933  paddss2  29934  pmapjoin  29968  pmapjat1  29969  cdleme36a  30576  dib2dim  31360  dih2dimbALTN  31362  djhcvat42  31532  dihjatcclem4  31538  dihjat1lem  31545  lcfrlem6  31664  hlhillcs  32078
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