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  2247  ax11inda2ALT  2248  unielrel  5353  fconst5  5908  soisores  6006  ovmpt2s  6156  caofrss  6296  caoftrn  6298  f1o2ndf1  6413  oaord  6749  omord2  6769  omcan  6771  oeord  6790  oecan  6791  nnaord  6821  nnmord  6834  omsmo  6856  ovec  6973  pmss12g  6999  cantnf  7605  pm54.43  7843  ttukeylem2  8346  axlttrn  9104  axltadd  9105  axmulgt0  9106  axsup  9107  ltadd2  9133  ltord1  9509  recex  9610  prodge0  9813  ltmul1  9816  lt2msq  9850  nnge1  9982  zltp1le  10281  uzss  10462  eluzp1m1  10465  ixxssixx  10886  zesq  11457  climrlim2  12296  rlimres  12307  climshftlem  12323  lo1add  12375  lo1mul  12376  rlimsqzlem  12397  lo1le  12400  isercolllem2  12414  isercoll  12416  climsup  12418  cvgcmp  12550  climcndslem1  12584  dvds1lem  12816  algcvg  13022  eucalgcvga  13032  rpexp12i  13077  crt  13122  pc2dvds  13207  pcmpt  13216  prmpwdvds  13227  1arith  13250  vdwlem2  13305  vdwlem6  13309  vdwlem8  13311  ercpbl  13729  ipopos  14541  subginv  14906  symggrp  15058  lsmless1x  15233  lsmless2x  15234  dprdss  15542  dvdsunit  15723  irredrmul  15767  isdrngd  15815  lspextmo  16087  domnchr  16768  zntoslem  16792  tgss  16988  neips  17132  opnnei  17139  lpss3  17163  ssrest  17194  t1t0  17366  kgen2ss  17540  isfild  17843  fgss  17858  fgss2  17859  cnpflf2  17985  fclsss1  18007  fclsss2  18008  tgpt0  18101  tsmsxp  18137  prdsxmslem2  18512  ngptgp  18630  nghmcn  18732  qdensere  18757  evth  18937  nmhmcn  19081  tchcph  19147  caussi  19203  equivcfil  19205  ivthlem2  19302  ovollb2lem  19337  ovolunlem1  19346  volun  19392  ioombl1lem4  19408  volsup2  19450  volcn  19451  ismbf3d  19499  itg2mulclem  19591  cpnord  19774  lhop1  19851  evlseu  19890  aaliou3lem2  20213  ulmclm  20256  ulmss  20266  abelth  20310  cosord  20387  efif1olem4  20400  argimgt0  20460  logdivlt  20469  cxploglim  20769  dvdssqf  20874  mumullem1  20915  mumullem2  20916  bposlem6  21026  lgsdchr  21085  m1lgs  21099  chtppilim  21122  nb3gra2nb  21417  spthispth  21526  wlkdvspth  21561  cycliscrct  21570  3v3e3cycl1  21584  4cycl4v4e  21606  4cycl4dv4e  21608  cusconngra  21616  eupatrl  21643  minvecolem5  22336  ocsh  22738  shless  22814  leopadd  23588  leopmuli  23589  leopmul2i  23591  leoptr  23593  spansncv2  23749  mdsl0  23766  ssdmd1  23769  cvdmd  23793  cdj3i  23897  cvmliftmolem1  24921  lediv2aALT  25070  relexp0  25082  predpo  25398  nodenselem5  25553  ax5seg  25781  axpasch  25784  axlowdimlem16  25800  axeuclid  25806  axcontlem4  25810  cgr3tr4  25890  colinearxfr  25913  lineext  25914  brsegle  25946  seglecgr12im  25948  segletr  25952  colinbtwnle  25956  outsideoftr  25967  lineelsb2  25986  itg2addnclem  26155  itg2addnclem3  26157  itg2addnc  26158  ivthALT  26228  tailfb  26296  incsequz  26342  mettrifi  26353  ismtycnv  26401  bfplem1  26421  ghomco  26448  rngoisocnv  26487  keridl  26532  dmncan1  26576  pell1234qrmulcl  26808  pell14qrss1234  26809  pell14qrmulcl  26816  pell14qrreccl  26817  pell1qrss14  26821  monotoddzzfi  26895  oddcomabszz  26897  f1otrspeq  27258  climinf  27599  swrdccatin12lem4  28025  swrdccatin12  28026  usgra2pthlem1  28040  frgra3vlem1  28104  3vfriswmgralem  28108  frgrawopreglem2  28148  usg2spot2nb  28168  2spotmdisj  28171  omllaw4  29729  cmtcomlemN  29731  cvlexch2  29812  cvlatexch2  29820  cvrexch  29902  atexchltN  29923  3atlem5  29969  lplnribN  30033  linepsubN  30234  paddss1  30299  paddss2  30300  pmapjoin  30334  pmapjat1  30335  cdleme36a  30942  dib2dim  31726  dih2dimbALTN  31728  djhcvat42  31898  dihjatcclem4  31904  dihjat1lem  31911  lcfrlem6  32030  hlhillcs  32444
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