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

Theorem 3imtr4i 266
Description: A mixed syllogism inference, useful for applying a definition to both sides of an implication. (Contributed by NM, 3-Jan-1993.)
Hypotheses
Ref Expression
3imtr4.1
3imtr4.2
3imtr4.3
Assertion
Ref Expression
3imtr4i

Proof of Theorem 3imtr4i
StepHypRef Expression
1 3imtr4.2 . . 3
2 3imtr4.1 . . 3
31, 2sylbi 195 . 2
4 3imtr4.3 . 2
53, 4sylibr 212 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184
This theorem is referenced by:  hbxfrbi  1643  sbimi  1745  ralimi2  2847  reximi2  2924  r19.28v  2991  r19.29r  2993  r19.30  3002  elex  3118  rmoan  3298  rmoimi2  3301  sseq2  3525  rabss2  3582  undif4  3883  r19.2zb  3919  ralf0  3936  difprsnss  4165  snsspw  4201  uniin  4269  intssOLD  4308  iuniin  4341  iuneq1  4344  iuneq2  4347  iunpwss  4420  eunex  4645  rmorabex  4712  exss  4715  pwunss  4790  soeq2  4825  elopaelxp  5077  reliin  5129  coeq1  5165  coeq2  5166  cnveq  5181  dmeq  5208  dmin  5215  dmcoss  5267  rncoeq  5271  dminss  5425  imainss  5426  dfco2a  5512  iotaex  5573  fununi  5659  fof  5800  f1ocnv  5833  isocnv  6226  isotr  6232  oprabid  6323  resiexg  6736  zfrep6  6768  ovmptss  6881  dmtpos  6986  tposfn  7003  smores  7042  omopthlem1  7323  eqer  7363  ixpeq2  7503  enssdom  7560  fiprc  7617  sbthlem9  7655  infensuc  7715  fipwuni  7906  zfreg  8042  zfreg2  8043  dfom3  8085  r1elss  8245  scott0  8325  fin56  8794  dominf  8846  ac6n  8886  brdom4  8929  dominfac  8969  inawina  9089  eltsk2g  9150  ltsosr  9492  ssxr  9675  ltadd2iOLD  9737  recgt0ii  10476  sup2  10524  dfnn2  10574  peano2uz2  10975  eluzp1p1  11135  peano2uz  11163  zq  11217  elfzmlbmOLD  11814  ubmelfzo  11881  expclzlem  12190  wrdeq  12564  wwlktovf  12894  fsum2dlem  13585  fprod2dlem  13784  sin02gt0  13927  divalglem6  14056  qredeu  14248  isfunc  15233  xpcbas  15447  drsdirfi  15567  clatl  15746  tsrss  15853  gimcnv  16315  gsum2dlem1  16997  gsum2dlem2  16998  gsum2dOLD  17000  lmimcnv  17713  xrge0subm  18459  fctop  19505  cctop  19507  alexsubALTlem4  20550  lpbl  21006  xrge0gsumle  21338  xrge0tsms  21339  iirev  21429  iihalf1  21431  iihalf2  21433  iimulcl  21437  vitalilem1  22017  ply1idom  22525  aacjcl  22723  aannenlem2  22725  ang180lem4  23144  lgslem3  23573  axlowdim  24264  axcontlem2  24268  usgraexmpl  24401  nmobndseqi  25694  axhcompl-zf  25915  hhcmpl  26117  shunssi  26286  spansni  26475  pjoml3i  26504  cmcmlem  26509  nonbooli  26569  lnopco0i  26923  pjnmopi  27067  pjnormssi  27087  hatomistici  27281  cvexchi  27288  cmdmdi  27336  mddmdin0i  27350  cdj3lem3b  27359  disjin  27446  xrge0tsmsd  27775  issgon  28123  sxbrsigalem0  28242  eulerpartlemgs2  28319  ballotlem2  28427  ballotth  28476  elpotr  29213  dfon2lem8  29222  sltval2  29416  txpss3v  29528  meran1  29876  arg-ax  29881  bndss  30282  fldcrng  30401  flddmn  30455  prter1  30620  mzpclall  30659  setindtrs  30967  dgraalem  31094  nzin  31223  axc11next  31313  iotaexeu  31325  reuan  32185  aovpcov0  32275  aov0ov0  32278  mhmismgmhm  32494  sgrpplusgaopALT  32519  rhmisrnghm  32726  srhmsubclem1  32881  srhmsubcOLDlem1  32900  rhmsubcOLDlem3  32915  hbexgVD  33706  bnj945  33832  bnj556  33958  bnj557  33959  bnj607  33974  bnj864  33980  bnj969  34004  bnj999  34015  bnj1398  34090  bj-nfalt  34265  bj-eunex  34385  bj-ifimim  37716  intimass  37768  psshepw  37811
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