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  2246  ax12inda2ALT  2247  unielrel  5362  fconst5  5935  soisores  6018  caofrss  6353  caoftrn  6355  f1o2ndf1  6680  oaord  6986  omord2  7006  omcan  7008  oeord  7027  oecan  7028  nnaord  7058  nnmord  7071  omsmo  7093  ovec  7210  pmss12g  7239  cantnf  7901  cantnfOLD  7923  pm54.43  8170  ttukeylem2  8679  axlttrn  9447  axltadd  9448  axmulgt0  9449  axsup  9450  ltadd2  9478  ltord1  9866  recex  9968  prodge0  10176  ltmul1  10179  lt2msq  10216  nnge1  10348  zltp1le  10694  uzss  10881  eluzp1m1  10884  ixxssixx  11314  zesq  11987  swrdccatin12lem3  12381  swrdccat3blem  12386  climrlim2  13025  rlimres  13036  climshftlem  13052  lo1add  13104  lo1mul  13105  rlimsqzlem  13126  lo1le  13129  isercolllem2  13143  isercoll  13145  climsup  13147  cvgcmp  13279  climcndslem1  13312  dvds1lem  13544  algcvg  13751  eucalgcvga  13761  rpexp12i  13808  crt  13853  pc2dvds  13945  pcmpt  13954  prmpwdvds  13965  1arith  13988  vdwlem2  14043  vdwlem6  14047  vdwlem8  14049  ercpbl  14487  ipopos  15330  subginv  15688  symggrp  15905  f1otrspeq  15953  lsmless1x  16143  lsmless2x  16144  dprdss  16526  dvdsunit  16755  irredrmul  16799  isdrngd  16857  lspextmo  17137  evlseu  17602  domnchr  17963  zntoslem  17989  tgss  18573  neips  18717  opnnei  18724  lpss3  18748  ssrest  18780  t1t0  18952  kgen2ss  19128  isfild  19431  fgss  19446  fgss2  19447  cnpflf2  19573  fclsss1  19595  fclsss2  19596  tgpt0  19689  tsmsxp  19729  prdsxmslem2  20104  ngptgp  20222  nghmcn  20324  qdensere  20349  evth  20531  nmhmcn  20675  tchcph  20752  caussi  20808  equivcfil  20810  ivthlem2  20936  ovollb2lem  20971  ovolunlem1  20980  volun  21026  ioombl1lem4  21042  volsup2  21085  volcn  21086  ismbf3d  21132  itg2mulclem  21224  cpnord  21409  lhop1  21486  aaliou3lem2  21809  ulmclm  21852  ulmss  21862  abelth  21906  cosord  21988  efif1olem4  22001  argimgt0  22061  logdivlt  22070  cxploglim  22371  dvdssqf  22476  mumullem1  22517  mumullem2  22518  bposlem6  22628  lgsdchr  22687  m1lgs  22701  chtppilim  22724  ax5seg  23184  axpasch  23187  axlowdimlem16  23203  axeuclid  23209  axcontlem4  23213  nb3gra2nb  23363  spthispth  23472  wlkdvspth  23507  cycliscrct  23516  3v3e3cycl1  23530  4cycl4v4e  23552  4cycl4dv4e  23554  cusconngra  23562  eupatrl  23589  minvecolem5  24282  ocsh  24686  shless  24762  leopadd  25536  leopmuli  25537  leopmul2i  25539  leoptr  25541  spansncv2  25697  mdsl0  25714  ssdmd1  25717  cvdmd  25741  cdj3i  25845  cvmliftmolem1  27170  lediv2aALT  27322  relexp0  27331  predpo  27645  nodenselem5  27826  cgr3tr4  28083  colinearxfr  28106  lineext  28107  brsegle  28139  seglecgr12im  28141  segletr  28145  colinbtwnle  28149  outsideoftr  28160  lineelsb2  28179  itg2addnclem  28443  itg2addnclem3  28445  itg2addnc  28446  ivthALT  28530  tailfb  28598  incsequz  28644  mettrifi  28653  ismtycnv  28701  bfplem1  28721  ghomco  28748  rngoisocnv  28787  keridl  28832  dmncan1  28876  pell1234qrmulcl  29196  pell14qrss1234  29197  pell14qrmulcl  29204  pell14qrreccl  29205  pell1qrss14  29209  monotoddzzfi  29283  oddcomabszz  29285  climinf  29779  fvelrnfvelrnressn  30151  2ffzoeq  30214  usgra2pthlem1  30300  erclwwlknsym  30500  erclwwlkntr  30501  clwlkfclwwlk  30517  frgra3vlem1  30592  3vfriswmgralem  30596  frgrawopreglem2  30638  usg2spot2nb  30658  2spotmdisj  30661  numclwwlk5  30705  omllaw4  32891  cmtcomlemN  32893  cvlexch2  32974  cvlatexch2  32982  cvrexch  33064  atexchltN  33085  3atlem5  33131  lplnribN  33195  linepsubN  33396  paddss1  33461  paddss2  33462  pmapjoin  33496  pmapjat1  33497  cdleme36a  34104  dib2dim  34888  dih2dimbALTN  34890  djhcvat42  35060  dihjatcclem4  35066  dihjat1lem  35073  lcfrlem6  35192  hlhillcs  35606
  Copyright terms: Public domain W3C validator