MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  3imtr4d 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
3imtr4d.2
3imtr4d.3
Assertion
Ref Expression
3imtr4d

Proof of Theorem 3imtr4d
StepHypRef Expression
1 3imtr4d.2 . 2
2 3imtr4d.1 . . 3
3 3imtr4d.3 . . 3
42, 3sylibrd 234 . 2
51, 4sylbid 215 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184
This theorem is referenced by:  ax12indalem  2275  ax12inda2ALT  2276  unielrel  5537  fvrnressn  6086  fconst5  6128  soisores  6223  caofrss  6573  caoftrn  6575  f1o2ndf1  6908  oaord  7215  omord2  7235  omcan  7237  oeord  7256  oecan  7257  nnaord  7287  nnmord  7300  omsmo  7322  pmss12g  7465  cantnf  8133  cantnfOLD  8155  pm54.43  8402  ttukeylem2  8911  axlttrn  9678  axltadd  9679  axmulgt0  9680  axsup  9681  ltadd2  9709  ltord1  10104  recex  10206  prodge0  10414  ltmul1  10417  lt2msq  10454  nnge1  10587  zltp1le  10938  uzss  11130  eluzp1m1  11133  ixxssixx  11572  zesq  12289  swrdccatin12lem3  12715  swrdccat3blem  12720  climrlim2  13370  rlimres  13381  climshftlem  13397  lo1add  13449  lo1mul  13450  rlimsqzlem  13471  lo1le  13474  isercolllem2  13488  isercoll  13490  climsup  13492  cvgcmp  13630  climcndslem1  13661  dvds1lem  13995  algcvg  14205  eucalgcvga  14215  rpexp12i  14263  crt  14308  pc2dvds  14402  pcmpt  14411  prmpwdvds  14422  1arith  14445  vdwlem2  14500  vdwlem6  14504  vdwlem8  14506  ercpbl  14946  ipopos  15790  subginv  16208  symggrp  16425  f1otrspeq  16472  lsmless1x  16664  lsmless2x  16665  dprdss  17076  dvdsunit  17312  irredrmul  17356  isdrngd  17421  lspextmo  17702  evlseu  18185  domnchr  18569  zntoslem  18595  mat2pmatf1  19230  tgss  19470  neips  19614  opnnei  19621  lpss3  19645  ssrest  19677  t1t0  19849  kgen2ss  20056  isfild  20359  fgss  20374  fgss2  20375  cnpflf2  20501  fclsss1  20523  fclsss2  20524  tgpt0  20617  tsmsxp  20657  prdsxmslem2  21032  ngptgp  21150  nghmcn  21252  qdensere  21277  evth  21459  nmhmcn  21603  tchcph  21680  caussi  21736  equivcfil  21738  rrxmvallem  21831  ivthlem2  21864  ovollb2lem  21899  ovolunlem1  21908  volun  21955  ioombl1lem4  21971  volsup2  22014  volcn  22015  ismbf3d  22061  itg2mulclem  22153  cpnord  22338  lhop1  22415  aaliou3lem2  22739  ulmclm  22782  ulmss  22792  abelth  22836  cosord  22919  efif1olem4  22932  argimgt0  22997  logdivlt  23006  cxploglim  23307  dvdssqf  23412  mumullem1  23453  mumullem2  23454  bposlem6  23564  lgsdchr  23623  m1lgs  23637  chtppilim  23660  ax5seg  24241  axpasch  24244  axlowdimlem16  24260  axeuclid  24266  axcontlem4  24270  elusuhgra  24368  nb3gra2nb  24455  spthispth  24575  wlkdvspth  24610  cycliscrct  24630  3v3e3cycl1  24644  4cycl4v4e  24666  4cycl4dv4e  24668  cusconngra  24676  erclwwlknsym  24826  erclwwlkntr  24827  clwlkfclwwlk  24844  eupatrl  24968  frgra3vlem1  25000  3vfriswmgralem  25004  frgrawopreglem2  25045  usg2spot2nb  25065  2spotmdisj  25068  numclwwlk5  25112  minvecolem5  25797  ocsh  26201  shless  26277  leopadd  27051  leopmuli  27052  leopmul2i  27054  leoptr  27056  spansncv2  27212  mdsl0  27229  ssdmd1  27232  cvdmd  27256  cdj3i  27360  cmpcref  27853  cvmliftmolem1  28726  mrsubff1  28874  msubff1  28916  lediv2aALT  29043  relexp0  29052  predpo  29264  nodenselem5  29445  cgr3tr4  29702  colinearxfr  29725  lineext  29726  brsegle  29758  seglecgr12im  29760  segletr  29764  colinbtwnle  29768  outsideoftr  29779  lineelsb2  29798  itg2addnclem  30066  itg2addnclem3  30068  itg2addnc  30069  ivthALT  30153  tailfb  30195  incsequz  30241  mettrifi  30250  ismtycnv  30298  bfplem1  30318  ghomco  30345  rngoisocnv  30384  keridl  30429  dmncan1  30473  pell1234qrmulcl  30791  pell14qrss1234  30792  pell14qrmulcl  30799  pell14qrreccl  30800  pell1qrss14  30804  monotoddzzfi  30878  oddcomabszz  30880  climinf  31612  2ffzoeq  32341  usgra2pthlem1  32353  usgo0s0  32435  usgo0s0ALT  32436  usgo1s0ALT  32437  usgo1s0  32442  usgfis  32446  initoid  32611  termoid  32612  omllaw4  34971  cmtcomlemN  34973  cvlexch2  35054  cvlatexch2  35062  cvrexch  35144  atexchltN  35165  3atlem5  35211  lplnribN  35275  linepsubN  35476  paddss1  35541  paddss2  35542  pmapjoin  35576  pmapjat1  35577  cdleme36a  36186  dib2dim  36970  dih2dimbALTN  36972  djhcvat42  37142  dihjatcclem4  37148  dihjat1lem  37155  lcfrlem6  37274  hlhillcs  37688
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
  Copyright terms: Public domain W3C validator